# Theory ML_Utils

theory ML_Utils
imports

begin

ML_file "utils.ML"

MLfun econtr_tac neg_thms ctxt =
let
val neg_thms = map (fn thm => @{thm notE} OF [thm]) neg_thms
in SOLVED' (eresolve_tac ctxt neg_thms) end

(* from HOL.thy *)
fun eval_tac ctxt =
let val conv = Code_Runtime.dynamic_holds_conv ctxt
in
CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
resolve_tac ctxt [TrueI]
end

lemma norm_all_conjunction:
"P Q. ((x. PROP P x) &&& PROP Q)  (x. PROP P x &&& PROP Q)"
"P Q. (PROP P &&& (x. PROP Q x))  (x. PROP P &&& PROP Q x)"
proof -
show "((x. PROP P x) &&& PROP Q)  (x. PROP P x &&& PROP Q)" for P Q
proof
fix x
assume "(x. PROP P x) &&& PROP Q"
note Pure.conjunctionD1[OF this, rule_format] Pure.conjunctionD2[OF this]
thus "PROP P x &&& PROP Q" .
next
assume "(x. PROP P x &&& PROP Q)"
note Pure.conjunctionD1[OF this] Pure.conjunctionD2[OF this]
thus "(x. PROP P x) &&& PROP Q" .
qed
next
show "(PROP P &&& (x. PROP Q x))  (x. PROP P &&& PROP Q x)" for P Q
proof
fix x
assume "PROP P &&& (x. PROP Q x)"
note Pure.conjunctionD1[OF this] Pure.conjunctionD2[OF this, rule_format]
thus "PROP P &&& PROP Q x" .
next
assume "(x. PROP P &&& PROP Q x)"
note Pure.conjunctionD1[OF this] Pure.conjunctionD2[OF this]
thus "PROP P &&& (x. PROP Q x)" .
qed
qed

MLfun norm_all_conjunction_tac ctxt =
CONVERSION (repeat1_conv (Dict_Construction_Util.changed_conv (Conv.top_sweep_conv
(K (Conv.rewrs_conv @{thms norm_all_conjunction})) ctxt)))

end

# File ‹utils.ML›

fun repeat1_conv cv = cv then_conv Conv.repeat_conv cv

fun init [] = error "empty list"
| init [_] = []
| init (x :: xs) = x :: init xs

fun last [] = error "empty list"
| last [x] = x
| last (_ :: xs) = last xs

val unvarify_typ =
let
fun aux (TVar ((name, idx), sort)) = TFree (name ^ Value.print_int idx, sort)
| aux t = t
in map_atyps aux end

fun all_consts (Const (name, typ)) = [(name, typ)]
| non_overlapping (_ $_) (Const _) = true | non_overlapping (t1$ t2) (u1 $u2) = non_overlapping t1 u1 orelse non_overlapping t2 u2 | non_overlapping _ _ = false fun extract thm = let val lhs = fst (Logic.dest_equals (Thm.prop_of thm)) val name = fst (dest_Const (fst (strip_comb lhs))) in (name, (lhs, thm)) end fun functrans ctxt thms = let val groups = AList.group op = (map extract thms) fun process_group (name, eqs) = let val const = Pretty.string_of (pretty_const ctxt name) fun pattern_renames (t1$ t2) (u1 $u2) = pattern_renames t1 u1 @ (if t1 = u1 then pattern_renames t2 u2 else []) | pattern_renames t u = if t = u orelse non_overlapping t u then [] else case t of Var (iname, _) => [(iname, u)] | _ => error ("Unsupported pattern situation in " ^ const) fun is_bogus_eq term = case term of (Const (@{const_name equal_class.equal}, _)$ t $u) => t = u andalso is_Var t | _ => false fun insert (lhs1, thm1) (changed, (lhss, thms)) = if is_bogus_eq lhs1 then (true, (lhss, thms)) else let val renamess = map (fn lhs2 => case pattern_renames lhs1 lhs2 of [] => NONE | xs => SOME xs) lhss |> cat_options fun rename renames = let val inst = map (fn (t, u) => (t, Thm.cterm_of ctxt u)) renames val msg = "Renaming pattern variables in " ^ const val _ = warning msg in Drule.infer_instantiate ctxt inst thm1 end in case renamess of [] => (changed, (lhs1 :: lhss, thm1 :: thms)) | [renames] => (true, (lhss, rename renames :: thms)) | _ => error ("Too many incompatible equations in " ^ const ^ ", this is unsupported") end in fold insert eqs (false, ([], [])) |> apsnd snd end val (changed, thms) = map process_group groups |> split_list |> apsnd flat |> apfst (exists I) in if changed then SOME thms else NONE end val enabled = setup_conditional_functrans @{binding pattern_compatibility} functrans end # File ‹dynamic_unfold.ML› signature DYNAMIC_UNFOLD = sig val enabled: bool Config.T val simproc: morphism -> Proof.context -> cterm -> thm option end structure Dynamic_Unfold : DYNAMIC_UNFOLD = struct val enabled = Attrib.setup_config_bool @{binding "dynamic_unfold"} (K false) open Dict_Construction_Util fun simproc _ ctxt ct = if Config.get ctxt enabled then let val ctxt = Config.put enabled false ctxt val thy = Proof_Context.theory_of ctxt val unfold_thms = all_consts (Thm.term_of ct) |> filter (not o can dest_funT o snd) |> map (snd o Code.equations_of_cert thy o Code.get_cert ctxt [] o fst) |> cat_options |> flat |> map (fst o snd) |> cat_options in if null unfold_thms then NONE else (* in principle this should *always* change something, but we better wrap it in changed_conv to at least throw an error instead of loop *) SOME (changed_conv (Raw_Simplifier.rewrite ctxt false unfold_thms) ct) end else NONE end # Theory CakeML_Utils theory CakeML_Utils imports begin type_synonym v_ns = "(modN, varN, v) namespace" type_synonym c_ns = "(modN, conN, (nat * tid_or_exn)) namespace" type_synonym all_env = "v sem_env" abbreviation cake_linear_clauses :: "(Ast.pat × exp) list bool" where "cake_linear_clauses list_all (λ(pat, _). allDistinct (pat_bindings pat []))" hide_const Lem_string.concat (* needed for the function package *) lemma [measure_function]: "is_measure (size_sem_env size)" by rule declare all_distinct_alt_def[simp] fun if_rval where "if_rval f (Rval v0) f v0" | "if_rval _ _ True" lemma if_rvalI: "(v. r = Rval v P v) if_rval P r" by (cases r) auto fun if_match where "if_match f (Match env) f env" | "if_match _ _ True" fun sequence_result :: "('a, 'b) result list ('a list, 'b) result" where "sequence_result [] = Rval []" | "sequence_result (Rerr err # rs) = Rerr err" | "sequence_result (Rval v0 # rs) = map_result (λvs. v0 # vs) id (sequence_result rs)" lemma sequence_result_rvalD[dest]: assumes "sequence_result rs = Rval vs" shows "rs = map Rval vs" using assms proof (induction rs arbitrary: vs) case (Cons r rs) then obtain v0 vs0 where "r = Rval v0" "vs = v0 # vs0" "sequence_result rs = Rval vs0" by (cases r; cases "sequence_result rs") auto with Cons show ?case by auto qed simp lemma sequence_result_Rval[simp]: "sequence_result (map Rval rs) = Rval rs" by (induction rs) auto (* FIXME move to CakeML entry *) context begin qualified definition tapp_0 where "tapp_0 tc = Tapp [] tc" qualified definition tapp_1 where "tapp_1 tc t1 = Tapp [t1] tc" qualified definition tapp_2 where "tapp_2 tc t1 t2 = Tapp [t1, t2] tc" end quickcheck_generator Ast.t constructors: Ast.Tvar, Ast.Tvar_db, CakeML_Utils.tapp_0, CakeML_Utils.tapp_1, CakeML_Utils.tapp_2 end # Theory Test_Utils theory Test_Utils imports Code_Utils Huffman.Huffman begin section ‹Dynamic unfolding› definition one :: nat where "one = 1" fun plus_one :: "nat nat" where "plus_one (Suc x) = one + plus_one x" | "plus_one _ = one" MLfun has_one ctxt = let val const = @{const_name plus_one} val {eqngr, ...} = Code_Preproc.obtain true {ctxt = ctxt, consts = [const], terms = []} val all_consts = Graph.all_succs eqngr [const] in member op = all_consts @{const_name one} end ML@{assert} (has_one @{context}) context notes [[dynamic_unfold]] begin ML@{assert} (not (has_one @{context})) end section ‹Pattern compatibility› subsection ‹Cannot deal with diagonal function› fun diagonal :: "_ _ _ nat" where "diagonal x True False = 1" | "diagonal False y True = 2" | "diagonal True False z = 3" code_thms diagonal code_thms Leftist_Heap.ltree context notes [[pattern_compatibility]] begin ML{ctxt = @{context}, consts = [@{const_name diagonal}], terms = []} |> can (Code_Preproc.obtain true) |> not |> @{assert} export_code huffman checking SML Scala export_code Leftist_Heap.ltree Leftist_Heap.node Leftist_Heap.merge Leftist_Heap.insert Leftist_Heap.del_min checking SML Scala export_code Pairing_Heap_Tree.link Pairing_Heap_Tree.pass1 Pairing_Heap_Tree.pass2 Pairing_Heap_Tree.is_root Pairing_Heap_Tree.pheap checking SML Scala export_code Root_Balanced_Tree.size_tree_tm Root_Balanced_Tree.inorder2_tm Root_Balanced_Tree.split_min_tm checking SML Scala end (* FIXME RBT *) (* FIXME move to Dict_Construction *) MLopen Dict_Construction_Util› lemma assumes "P" "Q" "R" shows "P Q R" apply (tactic (REPEAT_ALL_NEW (resolve_tac @{context} @{thms conjI}) CONTINUE_WITH [resolve_tac @{context} @{thms assms(1)}, resolve_tac @{context} @{thms assms(2)}, resolve_tac @{context} @{thms assms(3)}]) 1) done lemma assumes "P" "Q" "R" shows "P Q R" apply (tactic (REPEAT_ALL_NEW (resolve_tac @{context} @{thms conjI}) CONTINUE_WITH_FW [resolve_tac @{context} @{thms assms(1)}, K all_tac, resolve_tac @{context} @{thms assms(3)}]) 1) apply (rule assms(2)) done lemma assumes "P" "Q" shows "(P Q)" "(P Q)" apply (tactic ‹Goal.recover_conjunction_tac THEN (Goal.conjunction_tac THEN_ALL_NEW (REPEAT_ALL_NEW (resolve_tac @{context} @{thms conjI}) CONTINUE_WITH [resolve_tac @{context} @{thms assms(1)}, resolve_tac @{context} @{thms assms(2)}])) 1) done lemma assumes "Q" "P" shows "P Q" apply (tactic (resolve_tac @{context} @{thms conjI conjI[rotated]} CONTINUE_WITH [resolve_tac @{context} @{thms assms(1)}, resolve_tac @{context} @{thms assms(2)}]) 1) done end # Theory Doc_Terms chapter ‹Terms› theory Doc_Terms imports Main begin end # Theory Terms_Extras section ‹Additional material over the Higher_Order_Terms› AFP entry› theory Terms_Extras imports Higher_Order_Terms.Pats begin no_notation Mpat_Antiquot.mpaq_App (infixl "$$" 900) ML_file "hol_term.ML" primrec basic_rule :: "_ bool" where "basic_rule (lhs, rhs) linear lhs is_const (fst (strip_comb lhs)) ¬ is_const lhs frees rhs |⊆| frees lhs" lemma basic_ruleI[intro]: assumes "linear lhs" assumes "is_const (fst (strip_comb lhs))" assumes "¬ is_const lhs" assumes "frees rhs |⊆| frees lhs" shows "basic_rule (lhs, rhs)" using assms by simp primrec split_rule :: "(term × 'a) (name × (term list × 'a))" where "split_rule (lhs, rhs) = (let (name, args) = strip_comb lhs in (const_name name, (args, rhs)))" fun unsplit_rule :: "(name × (term list × 'a)) (term × 'a)" where "unsplit_rule (name, (args, rhs)) = (name$$ args, rhs)" lemma split_unsplit: "split_rule (unsplit_rule t) = t" by (induct t rule: unsplit_rule.induct) (simp add: strip_list_comb const_name_def) lemma unsplit_split: assumes "basic_rule r" shows "unsplit_rule (split_rule r) = r" using assms by (cases r) (simp add: split_beta) datatype pat = Patvar name | Patconstr name "pat list" fun mk_pat :: "term pat" where "mk_pat pat = (case strip_comb pat of (Const s, args) Patconstr s (map mk_pat args) | (Free s, []) Patvar s)" declare mk_pat.simps[simp del] lemma mk_pat_simps[simp]: "mk_pat (name $$args) = Patconstr name (map mk_pat args)" "mk_pat (Free name) = Patvar name" apply (auto simp: mk_pat.simps strip_list_comb_const) apply (simp add: const_term_def) done primrec patvars :: "pat name fset" where "patvars (Patvar name) = {| name |}" | "patvars (Patconstr _ ps) = ffUnion (fset_of_list (map patvars ps))" lemma mk_pat_frees: assumes "linear p" shows "patvars (mk_pat p) = frees p" using assms proof (induction p rule: linear_pat_induct) case (comb name args) have "map (patvars mk_pat) args = map frees args" using comb by force hence "fset_of_list (map (patvars mk_pat) args) = fset_of_list (map frees args)" by metis thus ?case by (simp add: freess_def) qed simp text ‹ This definition might seem a little counter-intuitive. Assume we have two defining equations of a function, e.g.\ @{term map}: @{prop "map f [] = []"} @{prop "map f (x # xs) = f x # map f xs"} The pattern "matrix" is compiled right-to-left. Equal patterns are grouped together. This definition is needed to avoid the following situation: @{prop "map f [] = []"} @{prop "map g (x # xs) = g x # map g xs"} While this is logically the same as above, the problem is that @{text f} and @{text g} are overlapping but distinct patterns. Hence, instead of grouping them together, they stay separate. This leads to overlapping patterns in the target language which will produce wrong results. One way to deal with this is to rename problematic variables before invoking the compiler. › fun pattern_compatible :: "term term bool" where "pattern_compatible (t1 t2) (u1 u2) pattern_compatible t1 u1 (t1 = u1 pattern_compatible t2 u2)" | "pattern_compatible t u t = u non_overlapping t u" lemmas pattern_compatible_simps[simp] = pattern_compatible.simps[folded app_term_def] lemmas pattern_compatible_induct = pattern_compatible.induct[case_names app_app] lemma pattern_compatible_refl[intro?]: "pattern_compatible t t" by (induct t) auto corollary pattern_compatile_reflP[intro!]: "reflp pattern_compatible" by (auto intro: pattern_compatible_refl reflpI) lemma pattern_compatible_cases[consumes 1]: assumes "pattern_compatible t u" obtains (eq) "t = u" | (non_overlapping) "non_overlapping t u" using assms proof (induction arbitrary: thesis rule: pattern_compatible_induct) case (app_app t1 t2 u1 u2) show ?case proof (cases "t1 = u1 t2 = u2") case True with app_app show thesis by simp next case False from app_app have "pattern_compatible t1 u1" "t1 = u1 pattern_compatible t2 u2" by auto with False have "non_overlapping (t1 t2) (u1 u2)" using app_app by (metis non_overlapping_appI1 non_overlapping_appI2) thus thesis by (rule app_app.prems(2)) qed qed auto inductive rev_accum_rel :: "('a 'a bool) 'a list 'a list bool" for R where nil: "rev_accum_rel R [] []" | snoc: "rev_accum_rel R xs ys (xs = ys R x y) rev_accum_rel R (xs @ [x]) (ys @ [y])" lemma rev_accum_rel_refl[intro]: "reflp R rev_accum_rel R xs xs" unfolding reflp_def by (induction xs rule: rev_induct) (auto intro: rev_accum_rel.intros) lemma rev_accum_rel_length: assumes "rev_accum_rel R xs ys" shows "length xs = length ys" using assms by induct auto context begin private inductive_cases rev_accum_relE[consumes 1, case_names nil snoc]: "rev_accum_rel P xs ys" lemma rev_accum_rel_butlast[intro]: assumes "rev_accum_rel P xs ys" shows "rev_accum_rel P (butlast xs) (butlast ys)" using assms by (cases rule: rev_accum_relE) (auto intro: rev_accum_rel.intros) lemma rev_accum_rel_snoc_eqE: "rev_accum_rel P (xs @ [a]) (xs @ [b]) P a b" by (auto elim: rev_accum_relE) end abbreviation patterns_compatible :: "term list term list bool" where "patterns_compatible rev_accum_rel pattern_compatible" abbreviation patterns_compatibles :: "(term list × 'a) fset bool" where "patterns_compatibles fpairwise (λ(pats1, _) (pats2, _). patterns_compatible pats1 pats2)" lemma pattern_compatible_combD: assumes "length xs = length ys" "pattern_compatible (list_comb f xs) (list_comb f ys)" shows "patterns_compatible xs ys" using assms by (induction xs ys rule: rev_induct2) (auto intro: rev_accum_rel.intros) lemma pattern_compatible_combI[intro]: assumes "patterns_compatible xs ys" "pattern_compatible f g" shows "pattern_compatible (list_comb f xs) (list_comb g ys)" using assms proof (induction rule: rev_accum_rel.induct) case (snoc xs ys x y) then have "pattern_compatible (list_comb f xs) (list_comb g ys)" by auto moreover have " pattern_compatible x y" if "list_comb f xs = list_comb g ys" proof (rule snoc, rule list_comb_semi_inj) show "length xs = length ys" using snoc by (auto dest: rev_accum_rel_length) qed fact ultimately show ?case by auto qed (auto intro: rev_accum_rel.intros) experiment begin ― ‹The above example can be made concrete here. In general, the following identity does not hold:› lemma "pattern_compatible t u t = u non_overlapping t u" apply rule apply (erule pattern_compatible_cases; simp) apply (erule disjE) apply (metis pattern_compatible_refl) oops ― ‹The counterexample:› definition "pats1 = [Free (Name ''f''), Const (Name ''nil'')]" definition "pats2 = [Free (Name ''g''), Const (Name ''cons'') Free (Name ''x'') Free (Name ''xs'')]" proposition "non_overlapping (list_comb c pats1) (list_comb c pats2)" unfolding pats1_def pats2_def apply (simp add: app_term_def) apply (rule non_overlapping_appI2) apply (rule non_overlapping_const_appI) done proposition "¬ patterns_compatible pats1 pats2" unfolding pats1_def pats2_def apply rule apply (erule rev_accum_rel.cases) apply simp apply auto apply (erule rev_accum_rel.cases) apply auto apply (erule rev_accum_rel.cases) apply auto apply (metis overlapping_var1I) done end abbreviation pattern_compatibles :: "(term × 'a) fset bool" where "pattern_compatibles fpairwise (λ(lhs1, _) (lhs2, _). pattern_compatible lhs1 lhs2)" corollary match_compatible_pat_eq: assumes "pattern_compatible t1 t2" "linear t1" "linear t2" assumes "match t1 u = Some env1" "match t2 u = Some env2" shows "t1 = t2" using assms by (metis pattern_compatible_cases match_overlapping) corollary match_compatible_env_eq: assumes "pattern_compatible t1 t2" "linear t1" "linear t2" assumes "match t1 u = Some env1" "match t2 u = Some env2" shows "env1 = env2" using assms by (metis match_compatible_pat_eq option.inject) corollary matchs_compatible_eq: assumes "patterns_compatible ts1 ts2" "linears ts1" "linears ts2" assumes "matchs ts1 us = Some env1" "matchs ts2 us = Some env2" shows "ts1 = ts2" "env1 = env2" proof - fix name have "match (name$$ ts1) (name $$us) = Some env1" "match (name$$ ts2) (name $$us) = Some env2" using assms by auto moreover have "length ts1 = length ts2" using assms by (metis matchs_some_eq_length) ultimately have "pattern_compatible (name$$ ts1) (name $$ts2)" using assms by (auto simp: const_term_def) moreover have "linear (name$$ ts1)" "linear (name $$ts2)" using assms by (auto intro: linear_list_comb') note * = calculation from * have "name$$ ts1 = name $$ts2" by (rule match_compatible_pat_eq) fact+ thus "ts1 = ts2" by (meson list_comb_inj_second injD) from * show "env1 = env2" by (rule match_compatible_env_eq) fact+ qed lemma compatible_find_match: assumes "pattern_compatibles (fset_of_list cs)" "list_all (linear fst) cs" "is_fmap (fset_of_list cs)" assumes "match pat t = Some env" "(pat, rhs) set cs" shows "find_match cs t = Some (env, pat, rhs)" using assms proof (induction cs arbitrary: pat rhs) case (Cons c cs) then obtain pat' rhs' where [simp]: "c = (pat', rhs')" by force have "find_match ((pat', rhs') # cs) t = Some (env, pat, rhs)" proof (cases "match pat' t") case None have "pattern_compatibles (fset_of_list cs)" using Cons by (force simp: fpairwise_alt_def) have "list_all (linear fst) cs" using Cons by (auto simp: list_all_iff) have "is_fmap (fset_of_list cs)" using Cons by (meson fset_of_list_subset is_fmap_subset set_subset_Cons) show ?thesis apply (simp add: None) apply (rule Cons) apply fact+ using Cons None by force next case (Some env') have "linear pat" "linear pat'" using Cons apply (metis Ball_set comp_apply fst_conv) using Cons by simp moreover from Cons have "pattern_compatible pat pat'" apply (cases "pat = pat'") apply (simp add: pattern_compatible_refl) unfolding fpairwise_alt_def by (force simp: fset_of_list_elem) ultimately have "env' = env" "pat' = pat" using match_compatible_env_eq match_compatible_pat_eq using Cons Some by blast+ with Cons have "rhs' = rhs" using is_fmapD by (metis c = (pat', rhs') fset_of_list_elem list.set_intros(1)) show ?thesis apply (simp add: Some) apply (intro conjI) by fact+ qed thus ?case unfolding c = _ . qed auto context "term" begin definition arity_compatible :: "'a 'a bool" where "arity_compatible t1 t2 = ( let (head1, pats1) = strip_comb t1; (head2, pats2) = strip_comb t2 in head1 = head2 length pats1 = length pats2 )" abbreviation arity_compatibles :: "('a × 'b) fset bool" where "arity_compatibles fpairwise (λ(lhs1, _) (lhs2, _). arity_compatible lhs1 lhs2)" definition head :: "'a name" where "head t const_name (fst (strip_comb t))" abbreviation heads_of :: "(term × 'a) fset name fset" where "heads_of rs (head fst) || rs" end definition arity :: "('a list × 'b) fset nat" where "arity rs = fthe_elem' ((length fst) || rs)" lemma arityI: assumes "fBall rs (λ(pats, _). length pats = n)" "rs {||}" shows "arity rs = n" proof - have "(length fst) || rs = {| n |}" using assms by force thus ?thesis unfolding arity_def fthe_elem'_eq by simp qed end # File ‹hol_term.ML› val mk_string = HOLogic.mk_string o Class_Graph.mangle fun mk_name n = @{const Name} mk_string n fun fsetT typ = Type (@{type_name fset}, [typ]) fun fmapT keyT valueT = Type (@{type_name fmap}, [keyT, valueT]) fun mk_fset typ xs = let fun f x xs = Const (@{const_name finsert}, typ --> fsetT typ --> fsetT typ) x xs val init = Const (@{const_name bot}, fsetT typ) in fold f xs init end fun mk_fmap (keyT, valueT) xs = let val fmapT = fmapT keyT valueT fun f (k, v) xs = Const (@{const_name fmupd}, keyT --> valueT --> fmapT --> fmapT) k v xs val init = Const (@{const_name fmempty}, fmapT) in fold f xs init end signature HOL_TERM = sig val mk_term: bool -> term -> term val mk_eq: term -> term val list_comb: term * term list -> term val strip_comb: term -> term * term list end structure HOL_Term : HOL_TERM = struct fun list_comb (f, xs) = fold (fn x => fn t => @{const App} t x) xs f fun strip_comb t = let fun go (@{const App} f x) = apsnd (cons f) (go x) | go t = (t, []) in apsnd rev (go t) end fun mk_term schematic t = let fun aux (Const (n, _)) = @{const Const} mk_name n | aux (Free (n, _)) = if schematic then error "free variables are not supported" else @{const Free} mk_name n | aux (Bound i) = @{const Bound} HOLogic.mk_number @{typ nat} i | aux (t u) = @{const App} aux t aux u | aux (Abs (_, _, t)) = @{const Abs} aux t | aux (Var ((n, i), _)) = if schematic then @{const Free} mk_name (n ^ "." ^ Value.print_int i) else error "schematic variables are not supported" in aux t end val mk_eq = HOLogic.mk_prod o @{apply 2} (mk_term true) o Logic.dest_equals end # Theory HOL_Datatype section ‹Reflecting HOL datatype definitions› theory HOL_Datatype imports Terms_Extras begin datatype "typ" = TVar name | TApp name "typ list" datatype_compat "typ" context begin qualified definition tapp_0 where "tapp_0 tc = TApp tc []" qualified definition tapp_1 where "tapp_1 tc t1 = TApp tc [t1]" qualified definition tapp_2 where "tapp_2 tc t1 t2 = TApp tc [t1, t2]" end quickcheck_generator "typ" constructors: TVar, HOL_Datatype.tapp_0, HOL_Datatype.tapp_1, HOL_Datatype.tapp_2 datatype_record dt_def = tparams :: "name list" constructors :: "(name, typ list) fmap" ML_file "hol_datatype.ML" end # File ‹hol_datatype.ML› signature HOL_DATATYPE = sig val mk_typ: bool -> typ -> term val mk_dt_def: Proof.context -> string -> term end structure HOL_Datatype : HOL_DATATYPE = struct fun check_sort [@{class type}] = () | check_sort _ = error "non-standard sorts are not supported" fun mk_tvar ((name, idx), sort) = (check_sort sort; mk_name (name ^ "." ^ Value.print_int idx)) fun mk_tfree (name, sort) = (check_sort sort; mk_name name) fun mk_typ schematic t = let fun aux (Type (typ, args)) = @{const TApp} mk_name typ HOLogic.mk_list @{typ typ} (map aux args) | aux (TVar tvar) = if schematic then @{const TVar} mk_tvar tvar else error "schematic type variables are not supported" | aux (TFree tfree) = if schematic then error "free type variables are not supported" else @{const TVar} mk_tfree tfree in aux t end fun mk_dt_def ctxt typ = let val {ctrs, T, ...} = the (Ctr_Sugar.ctr_sugar_of ctxt typ) val tparams = dest_Type T |> snd |> map (mk_tvar o dest_TVar) |> HOLogic.mk_list @{typ name} fun mk_ctr ctr = let val (name, typ) = dest_Const ctr val params = strip_type typ |> fst |> map (mk_typ true) |> HOLogic.mk_list @{typ typ} in (mk_name name, params) end val ctrs = map mk_ctr ctrs |> mk_fmap (@{typ name}, @{typ "typ list"}) in @{const make_dt_def} tparams ctrs end end # Theory Constructors section ‹Constructor information› theory Constructors imports Terms_Extras HOL_Datatype begin type_synonym C_info = "(name, dt_def) fmap" locale constructors = fixes C_info :: C_info begin definition flat_C_info :: "(string × nat × string) list" where "flat_C_info = do { (tname, Cs) sorted_list_of_fmap C_info; (C, params) sorted_list_of_fmap (constructors Cs); [(as_string C, (length params, as_string tname))] }" definition all_tdefs :: "name fset" where "all_tdefs = fmdom C_info" definition C :: "name fset" where "C = ffUnion (fmdom || constructors || fmran C_info)" definition all_constructors :: "name list" where "all_constructors = concat (map (λ(_, Cs). map fst (sorted_list_of_fmap (constructors Cs))) (sorted_list_of_fmap C_info))" (* FIXME nice to have *) (* lemma all_constructors_alt_def: "all_constructors = map (Name ∘ fst) flat_C_info" unfolding all_constructors_def flat_C_info_def *) end declare constructors.C_def[code] declare constructors.flat_C_info_def[code] declare constructors.all_constructors_def[code] export_code constructors.C constructors.flat_C_info constructors.all_constructors checking Scala end # Theory Consts section ‹Special constants› theory Consts imports Constructors Higher_Order_Terms.Nterm begin locale special_constants = constructors locale pre_constants = special_constants + fixes heads :: "name fset" begin definition all_consts :: "name fset" where "all_consts = heads |∪| C" abbreviation welldefined :: "'a::term bool" where "welldefined t consts t |⊆| all_consts" sublocale welldefined: simple_syntactic_and welldefined by standard auto end declare pre_constants.all_consts_def[code] locale constants = pre_constants + assumes disjnt: "fdisjnt heads C" ― ‹Conceptually the following assumptions should belong into @{locale constructors}, but I prefer to keep that one assumption-free.› assumes distinct_ctr: "distinct all_constructors" begin lemma distinct_ctr': "distinct (map as_string all_constructors)" unfolding distinct_map using distinct_ctr by (auto intro: inj_onI dest: name.expand) end end # Theory Strong_Term section ‹Term algebra extended with wellformedness› theory Strong_Term imports Consts begin class pre_strong_term = "term" + fixes wellformed :: "'a bool" fixes all_frees :: "'a name fset" assumes wellformed_const[simp]: "wellformed (const name)" assumes wellformed_free[simp]: "wellformed (free name)" assumes wellformed_app[simp]: "wellformed (app u1 u2) wellformed u1 wellformed u2" assumes all_frees_const[simp]: "all_frees (const name) = fempty" assumes all_frees_free[simp]: "all_frees (free name) = {| name |}" assumes all_frees_app[simp]: "all_frees (app u1 u2) = all_frees u1 |∪| all_frees u2" begin abbreviation wellformed_env :: "(name, 'a) fmap bool" where "wellformed_env fmpred (λ_. wellformed)" end context pre_constants begin definition shadows_consts :: "'a::pre_strong_term bool" where "shadows_consts t ¬ fdisjnt all_consts (all_frees t)" sublocale shadows: simple_syntactic_or shadows_consts by standard (auto simp: shadows_consts_def fdisjnt_alt_def) abbreviation not_shadows_consts_env :: "(name, 'a::pre_strong_term) fmap bool" where "not_shadows_consts_env fmpred (λ_ s. ¬ shadows_consts s)" end declare pre_constants.shadows_consts_def[code] class strong_term = pre_strong_term + assumes raw_frees_all_frees: "abs_pred (λt. frees t |⊆| all_frees t) t" assumes raw_subst_wellformed: "abs_pred (λt. wellformed t (env. wellformed_env env wellformed (subst t env))) t" begin lemma frees_all_frees: "frees t |⊆| all_frees t" proof (induction t rule: raw_induct) case (abs t) show ?case by (rule raw_frees_all_frees) qed auto lemma subst_wellformed: "wellformed t wellformed_env env wellformed (subst t env)" proof (induction t arbitrary: env rule: raw_induct) case (abs t) show ?case by (rule raw_subst_wellformed) qed (auto split: option.splits) end global_interpretation wellformed: subst_syntactic_and "wellformed :: 'a::strong_term bool" by standard (auto simp: subst_wellformed) instantiation "term" :: strong_term begin fun all_frees_term :: "term name fset" where "all_frees_term (Free x) = {| x |}" | "all_frees_term (t1 t2) = all_frees_term t1 |∪| all_frees_term t2" | "all_frees_term (Λ t) = all_frees_term t" | "all_frees_term _ = {||}" lemma frees_all_frees_term[simp]: "all_frees t = frees (t::term)" by (induction t) auto definition wellformed_term :: "term bool" where [simp]: "wellformed_term t Term.wellformed t" instance proof (standard, goal_cases) case 8 (* FIXME move upstream *) have *: "abs_pred P t" if "P t" for P and t :: "term" unfolding abs_pred_term_def using that by auto show ?case apply (rule *) unfolding wellformed_term_def by (auto simp: Term.subst_wellformed) qed (auto simp: const_term_def free_term_def app_term_def abs_pred_term_def) end instantiation nterm :: strong_term begin definition wellformed_nterm :: "nterm bool" where [simp]: "wellformed_nterm t True" fun all_frees_nterm :: "nterm name fset" where "all_frees_nterm (Nvar x) = {| x |}" | "all_frees_nterm (t1 n t2) = all_frees_nterm t1 |∪| all_frees_nterm t2" | "all_frees_nterm (Λn x. t) = finsert x (all_frees_nterm t)" | "all_frees_nterm (Nconst _) = {||}" instance proof (standard, goal_cases) case (7 t) show ?case unfolding abs_pred_nterm_def by auto qed (auto simp: const_nterm_def free_nterm_def app_nterm_def abs_pred_nterm_def) end lemma (in pre_constants) shadows_consts_frees: fixes t :: "'a::strong_term" shows "¬ shadows_consts t fdisjnt all_consts (frees t)" unfolding fdisjnt_alt_def shadows_consts_def using frees_all_frees by auto abbreviation wellformed_clauses :: "_ bool" where "wellformed_clauses cs list_all (λ(pat, t). linear pat wellformed t) cs distinct (map fst cs) cs []" end # Theory Sterm section ‹Terms with sequential pattern matching› theory Sterm imports Strong_Term begin datatype sterm = Sconst name | Svar name | Sabs (clauses: "(term × sterm) list") | Sapp sterm sterm (infixl "s" 70) datatype_compat sterm derive linorder sterm abbreviation Sabs_single ("Λs _. _" [0, 50] 50) where "Sabs_single x rhs Sabs [(Free x, rhs)]" type_synonym sclauses = "(term × sterm) list" lemma sterm_induct[case_names Sconst Svar Sabs Sapp]: assumes "x. P (Sconst x)" assumes "x. P (Svar x)" assumes "cs. (pat t. (pat, t) set cs P t) P (Sabs cs)" assumes "t u. P t P u P (t s u)" shows "P t" using assms apply induction_schema apply pat_completeness apply lexicographic_order done instantiation sterm :: pre_term begin definition app_sterm where "app_sterm t u = t s u" fun unapp_sterm where "unapp_sterm (t s u) = Some (t, u)" | "unapp_sterm _ = None" definition const_sterm where "const_sterm = Sconst" fun unconst_sterm where "unconst_sterm (Sconst name) = Some name" | "unconst_sterm _ = None" fun unfree_sterm where "unfree_sterm (Svar name) = Some name" | "unfree_sterm _ = None" definition free_sterm where "free_sterm = Svar" fun frees_sterm where "frees_sterm (Svar name) = {|name|}" | "frees_sterm (Sconst _) = {||}" | "frees_sterm (Sabs cs) = ffUnion (fset_of_list (map (λ(pat, rhs). frees_sterm rhs - frees pat) cs))" | "frees_sterm (t s u) = frees_sterm t |∪| frees_sterm u" fun subst_sterm where "subst_sterm (Svar s) env = (case fmlookup env s of Some t t | None Svar s)" | "subst_sterm (t1 s t2) env = subst_sterm t1 env s subst_sterm t2 env" | "subst_sterm (Sabs cs) env = Sabs (map (λ(pat, rhs). (pat, subst_sterm rhs (fmdrop_fset (frees pat) env))) cs)" | "subst_sterm t env = t" fun consts_sterm :: "sterm name fset" where "consts_sterm (Svar _) = {||}" | "consts_sterm (Sconst name) = {|name|}" | "consts_sterm (Sabs cs) = ffUnion (fset_of_list (map (λ(_, rhs). consts_sterm rhs) cs))" | "consts_sterm (t s u) = consts_sterm t |∪| consts_sterm u" instance by standard (auto simp: app_sterm_def const_sterm_def free_sterm_def elim: unapp_sterm.elims unconst_sterm.elims unfree_sterm.elims split: option.splits) end instantiation sterm :: "term" begin definition abs_pred_sterm :: "(sterm bool) sterm bool" where [code del]: "abs_pred P t (cs. t = Sabs cs (pat t. (pat, t) set cs P t) P t)" lemma abs_pred_stermI[intro]: assumes "cs. (pat t. (pat, t) set cs P t) P (Sabs cs)" shows "abs_pred P t" using assms unfolding abs_pred_sterm_def by auto instance proof (standard, goal_cases) case (1 P t) then show ?case by (induction t) (auto simp: const_sterm_def free_sterm_def app_sterm_def abs_pred_sterm_def) next case (2 t) show ?case apply rule apply auto apply (subst (3) list.map_id[symmetric]) apply (rule list.map_cong0) apply auto by blast next case (3 x t) show ?case apply rule apply clarsimp subgoal for cs env pat rhs apply (cases "x |∈| frees pat") subgoal apply (rule arg_cong[where f = "subst rhs"]) by (auto intro: fmap_ext) subgoal premises prems[rule_format] apply (subst (2) prems(1)[symmetric, where pat = pat]) subgoal by fact subgoal using prems unfolding ffUnion_alt_def by (auto simp add: fmember.rep_eq fset_of_list.rep_eq elim!: fBallE) subgoal apply (rule arg_cong[where f = "subst rhs"]) by (auto intro: fmap_ext) done done done next case (4 t) show ?case apply rule apply clarsimp subgoal premises prems[rule_format] apply (rule prems(1)[OF prems(4)]) subgoal using prems by auto subgoal using prems unfolding fdisjnt_alt_def by auto done done next case 5 show ?case proof (intro abs_pred_stermI allI impI, goal_cases) case (1 cs env) show ?case proof safe fix name assume "name |∈| frees (subst (Sabs cs) env)" then obtain pat rhs where "(pat, rhs) set cs" and "name |∈| frees (subst rhs (fmdrop_fset (frees pat) env))" and "name |∉| frees pat" by (auto simp: fset_of_list_elem case_prod_twice comp_def ffUnion_alt_def) hence "name |∈| frees rhs |-| fmdom (fmdrop_fset (frees pat) env)" using 1 by (simp add: fmpred_drop_fset) hence "name |∈| frees rhs |-| frees pat" using name |∉| frees pat by blast show "name |∈| frees (Sabs cs)" apply (simp add: ffUnion_alt_def) apply (rule fBexI[where x = "(pat, rhs)"]) unfolding prod.case apply (fact name |∈| frees rhs |-| frees pat) unfolding fset_of_list_elem by fact assume "name |∈| fmdom env" thus False using name |∈| frees rhs |-| fmdom (fmdrop_fset (frees pat) env) name |∉| frees pat by fastforce next fix name assume "name |∈| frees (Sabs cs)" "name |∉| fmdom env" then obtain pat rhs where "(pat, rhs) set cs" "name |∈| frees rhs" "name |∉| frees pat" by (auto simp: fset_of_list_elem ffUnion_alt_def) moreover hence "name |∈| frees rhs |-| fmdom (fmdrop_fset (frees pat) env) |-| frees pat" using name |∉| fmdom env by fastforce ultimately have "name |∈| frees (subst rhs (fmdrop_fset (frees pat) env)) |-| frees pat" using 1 by (simp add: fmpred_drop_fset) show "name |∈| frees (subst (Sabs cs) env)" apply (simp add: case_prod_twice comp_def) unfolding ffUnion_alt_def apply (rule fBexI) apply (fact name |∈| frees (subst rhs (fmdrop_fset (frees pat) env)) |-| frees pat) apply (subst fimage_iff) apply (rule fBexI[where x = "(pat, rhs)"]) apply simp using (pat, rhs) set cs by (auto simp: fset_of_list_elem) qed qed next case 6 show ?case proof (intro abs_pred_stermI allI impI, goal_cases) case (1 cs env) ― ‹some property on various operations that is only useful in here› have *: "fbind (fmimage m (fbind A g)) f = fbind A (λx. fbind (fmimage m (g x)) f)" for m A f g including fset.lifting fmap.lifting by transfer' force have "consts (subst (Sabs cs) env) = fbind (fset_of_list cs) (λ(pat, rhs). consts rhs |∪| ffUnion (consts || fmimage (fmdrop_fset (frees pat) env) (frees rhs)))" apply (simp add: funion_image_bind_eq) apply (rule fbind_cong[OF refl]) apply (clarsimp split: prod.splits) apply (subst 1) apply (subst (asm) fset_of_list_elem, assumption) apply simp by (simp add: funion_image_bind_eq) also have " = fbind (fset_of_list cs) (consts snd) |∪| fbind (fset_of_list cs) (λ(pat, rhs). ffUnion (consts || fmimage (fmdrop_fset (frees pat) env) (frees rhs)))" apply (subst fbind_fun_funion[symmetric]) apply (rule fbind_cong[OF refl]) by auto also have " = consts (Sabs cs) |∪| fbind (fset_of_list cs) (λ(pat, rhs). ffUnion (consts || fmimage (fmdrop_fset (frees pat) env) (frees rhs)))" apply (rule cong[OF cong, OF refl _ refl, where f1 = "funion"]) apply (subst funion_image_bind_eq[symmetric]) unfolding consts_sterm.simps apply (rule arg_cong[where f = ffUnion]) apply (subst fset_of_list_map) apply (rule fset.map_cong[OF refl]) by auto also have " = consts (Sabs cs) |∪| fbind (fmimage env (fbind (fset_of_list cs) (λ(pat, rhs). frees rhs |-| frees pat))) consts" apply (subst funion_image_bind_eq) apply (subst fmimage_drop_fset) apply (rule cong[OF cong, OF refl refl, where f1 = "funion"]) apply (subst *) apply (rule fbind_cong[OF refl]) by auto also have " = consts (Sabs cs) |∪| ffUnion (consts || fmimage env (frees (Sabs cs)))" by (simp only: frees_sterm.simps fset_of_list_map fmimage_Union funion_image_bind_eq) finally show ?case . qed qed (auto simp: abs_pred_sterm_def) end lemma no_abs_abs[simp]: "¬ no_abs (Sabs cs)" by (subst no_abs.simps) (auto simp: term_cases_def) lemma closed_except_simps: "closed_except (Svar x) S x |∈| S" "closed_except (t1 s t2) S closed_except t1 S closed_except t2 S" "closed_except (Sabs cs) S list_all (λ(pat, t). closed_except t (S |∪| frees pat)) cs" "closed_except (Sconst name) S True" proof goal_cases case 3 show ?case proof (standard, goal_cases) case 1 then show ?case apply (auto simp: list_all_iff ffUnion_alt_def fset_of_list_elem closed_except_def) apply (drule ffUnion_least_rev) apply auto by (smt case_prod_conv fbspec fimageI fminusI fset_of_list_elem fset_rev_mp) next case 2 then show ?case by (fastforce simp: list_all_iff ffUnion_alt_def fset_of_list_elem closed_except_def) qed qed (auto simp: ffUnion_alt_def closed_except_def) lemma closed_except_sabs: assumes "closed (Sabs cs)" "(pat, rhs) set cs" shows "closed_except rhs (frees pat)" using assms unfolding closed_except_def apply auto by (metis bot.extremum_uniqueI fempty_iff ffUnion_subset_elem fimageI fminusI fset_of_list_elem old.prod.case) instantiation sterm :: strong_term begin fun wellformed_sterm :: "sterm bool" where "wellformed_sterm (t1 s t2) wellformed_sterm t1 wellformed_sterm t2" | "wellformed_sterm (Sabs cs) list_all (λ(pat, t). linear pat wellformed_sterm t) cs distinct (map fst cs) cs []" | "wellformed_sterm _ True" primrec all_frees_sterm :: "sterm name fset" where "all_frees_sterm (Svar x) = {|x|}" | "all_frees_sterm (t1 s t2) = all_frees_sterm t1 |∪| all_frees_sterm t2" | "all_frees_sterm (Sabs cs) = ffUnion (fset_of_list (map (λ(P, T). P |∪| T) (map (map_prod frees all_frees_sterm) cs)))" | "all_frees_sterm (Sconst _) = {||}" instance proof (standard, goal_cases) case (7 t) show ?case apply (intro abs_pred_stermI allI impI) apply simp apply (rule ffUnion_least) apply (rule fBallI) apply auto apply (subst ffUnion_alt_def) apply simp apply (rule_tac x = "(a, b)" in fBexI) by (auto simp: fset_of_list_elem) next case (8 t) show ?case apply (intro abs_pred_stermI allI impI) apply (simp add: list.pred_map comp_def case_prod_twice, safe) subgoal apply (subst list_all_iff) apply (rule ballI) apply safe[1] apply (fastforce simp: list_all_iff) subgoal premises prems[rule_format] apply (rule prems) apply (fact prems) using prems apply (fastforce simp: list_all_iff) using prems by force done subgoal apply (subst map_cong[OF refl]) by auto done qed (auto simp: const_sterm_def free_sterm_def app_sterm_def) end lemma match_sabs[simp]: "¬ is_free t match t (Sabs cs) = None" by (cases t) auto context pre_constants begin lemma welldefined_sabs: "welldefined (Sabs cs) list_all (λ(_, t). welldefined t) cs" apply (auto simp: list_all_iff ffUnion_alt_def dest!: ffUnion_least_rev) apply (subst (asm) list_all_iff_fset[symmetric]) apply (auto simp: list_all_iff fset_of_list_elem) done lemma shadows_consts_sterm_simps[simp]: "shadows_consts (t1 s t2) shadows_consts t1 shadows_consts t2" "shadows_consts (Svar name) name |∈| all_consts" "shadows_consts (Sabs cs) list_ex (λ(pat, t). ¬ fdisjnt all_consts (frees pat) shadows_consts t) cs" "shadows_consts (Sconst name) False" proof (goal_cases) case 3 show ?case unfolding shadows_consts_def list_ex_iff apply rule subgoal by (force simp: ffUnion_alt_def fset_of_list_elem fdisjnt_alt_def elim!: ballE) subgoal apply (auto simp: fset_of_list_elem fdisjnt_alt_def) by (auto simp: fset_eq_empty_iff ffUnion_alt_def fset_of_list_elem elim!: allE fBallE) done qed (auto simp: shadows_consts_def fdisjnt_alt_def) (* FIXME derive from axioms? *) lemma subst_shadows: assumes "¬ shadows_consts (t::sterm)" "not_shadows_consts_env Γ" shows "¬ shadows_consts (subst t Γ)" using assms proof (induction t arbitrary: Γ rule: sterm_induct) case (Sabs cs) show ?case apply (simp add: list_ex_iff case_prod_twice) apply (rule ballI) subgoal for c apply (cases c, hypsubst_thin, simp) apply (rule conjI) subgoal using Sabs(2) by (fastforce simp: list_ex_iff) apply (rule Sabs(1)) apply assumption subgoal using Sabs(2) by (fastforce simp: list_ex_iff) subgoal using Sabs(3) by force done done qed (auto split: option.splits) end end # Theory Pterm section ‹Terms with explicit pattern matching› theory Pterm imports Consts Sterm ― ‹Inclusion of this theory might seem a bit strange. Indeed, it is only for technical reasons: to allow for a quickcheck setup.› begin datatype pterm = Pconst name | Pvar name | Pabs "(term × pterm) fset" | Papp pterm pterm (infixl "p" 70) primrec sterm_to_pterm :: "sterm pterm" where "sterm_to_pterm (Sconst name) = Pconst name" | "sterm_to_pterm (Svar name) = Pvar name" | "sterm_to_pterm (t s u) = sterm_to_pterm t p sterm_to_pterm u" | "sterm_to_pterm (Sabs cs) = Pabs (fset_of_list (map (map_prod id sterm_to_pterm) cs))" quickcheck_generator pterm ― ‹will print some fishy constructor'' names, but at least it works› constructors: sterm_to_pterm lemma sterm_to_pterm_total: obtains t' where "t = sterm_to_pterm t'" proof (induction t arbitrary: thesis) case (Pconst x) then show ?case by (metis sterm_to_pterm.simps) next case (Pvar x) then show ?case by (metis sterm_to_pterm.simps) next case (Pabs cs) from Pabs.IH obtain cs' where "cs = fset_of_list (map (map_prod id sterm_to_pterm) cs')" apply atomize_elim proof (induction cs) case empty show ?case apply (rule exI[where x = "[]"]) by simp next case (insert c cs) obtain pat rhs where "c = (pat, rhs)" by (cases c) auto have "cs'. cs = fset_of_list (map (map_prod id sterm_to_pterm) cs')" apply (rule insert) using insert.prems unfolding finsert.rep_eq by blast then obtain cs' where "cs = fset_of_list (map (map_prod id sterm_to_pterm) cs')" by blast obtain rhs' where "rhs = sterm_to_pterm rhs'" apply (rule insert.prems[of "(pat, rhs)" rhs]) unfolding c = _ by simp+ show ?case apply (rule exI[where x = "(pat, rhs') # cs'"]) unfolding c = _ cs = _ rhs = _ by (simp add: id_def) qed hence "Pabs cs = sterm_to_pterm (Sabs cs')" by simp then show ?case using Pabs by metis next case (Papp t1 t2) then obtain t1' t2' where "t1 = sterm_to_pterm t1'" "t2 = sterm_to_pterm t2'" by metis then have "t1 p t2 = sterm_to_pterm (t1' s t2')" by simp with Papp show ?case by metis qed lemma pterm_induct[case_names Pconst Pvar Pabs Papp]: assumes "x. P (Pconst x)" assumes "x. P (Pvar x)" assumes "cs. (pat t. (pat, t) |∈| cs P t) P (Pabs cs)" assumes "t u. P t P u P (t p u)" shows "P t" proof (rule pterm.induct, goal_cases) case (3 cs) show ?case apply (rule assms) using 3 apply (subst (asm) fmember.rep_eq[symmetric]) by auto qed fact+ instantiation pterm :: pre_term begin definition app_pterm where "app_pterm t u = t p u" fun unapp_pterm where "unapp_pterm (t p u) = Some (t, u)" | "unapp_pterm _ = None" definition const_pterm where "const_pterm = Pconst" fun unconst_pterm where "unconst_pterm (Pconst name) = Some name" | "unconst_pterm _ = None" definition free_pterm where "free_pterm = Pvar" fun unfree_pterm where "unfree_pterm (Pvar name) = Some name" | "unfree_pterm _ = None" function (sequential) subst_pterm where "subst_pterm (Pvar s) env = (case fmlookup env s of Some t t | None Pvar s)" | "subst_pterm (t1 p t2) env = subst_pterm t1 env p subst_pterm t2 env" | "subst_pterm (Pabs cs) env = Pabs ((λ(pat, rhs). (pat, subst_pterm rhs (fmdrop_fset (frees pat) env))) || cs)" | "subst_pterm t _ = t" by pat_completeness auto termination proof (relation "measure (size fst)", goal_cases) case 4 then show ?case apply auto including fset.lifting apply transfer apply (rule le_imp_less_Suc) apply (rule sum_nat_le_single[where y = "(a, (b, size b))" for a b]) by auto qed auto primrec consts_pterm :: "pterm name fset" where "consts_pterm (Pconst x) = {|x|}" | "consts_pterm (t1 p t2) = consts_pterm t1 |∪| consts_pterm t2" | "consts_pterm (Pabs cs) = ffUnion (snd || map_prod id consts_pterm || cs)" | "consts_pterm (Pvar _) = {||}" primrec frees_pterm :: "pterm name fset" where "frees_pterm (Pvar x) = {|x|}" | "frees_pterm (t1 p t2) = frees_pterm t1 |∪| frees_pterm t2" | "frees_pterm (Pabs cs) = ffUnion ((λ(pv, tv). tv - frees pv) || map_prod id frees_pterm || cs)" | "frees_pterm (Pconst _) = {||}" instance by standard (auto simp: app_pterm_def const_pterm_def free_pterm_def elim: unapp_pterm.elims unconst_pterm.elims unfree_pterm.elims split: option.splits) end corollary subst_pabs_id: assumes "pat rhs. (pat, rhs) |∈| cs subst rhs (fmdrop_fset (frees pat) env) = rhs" shows "subst (Pabs cs) env = Pabs cs" apply (subst subst_pterm.simps) apply (rule arg_cong[where f = Pabs]) apply (rule fset_map_snd_id) apply (rule assms) apply (subst (asm) fmember.rep_eq[symmetric]) apply assumption done corollary frees_pabs_alt_def: "frees (Pabs cs) = ffUnion ((λ(pat, rhs). frees rhs - frees pat) || cs)" apply simp apply (rule arg_cong[where f = ffUnion]) apply (rule fset.map_cong[OF refl]) by auto lemma sterm_to_pterm_frees[simp]: "frees (sterm_to_pterm t) = frees t" proof (induction t) case (Sabs cs) show ?case apply simp apply (rule arg_cong[where f = ffUnion]) apply (rule fimage_cong[OF refl]) apply clarsimp apply (subst Sabs) by (auto simp: fset_of_list_elem snds.simps) qed auto lemma sterm_to_pterm_consts[simp]: "consts (sterm_to_pterm t) = consts t" proof (induction t) case (Sabs cs) show ?case apply simp apply (rule arg_cong[where f = ffUnion]) apply (rule fimage_cong[OF refl]) apply clarsimp apply (subst Sabs) by (auto simp: fset_of_list_elem snds.simps) qed auto lemma subst_sterm_to_pterm: "subst (sterm_to_pterm t) (fmmap sterm_to_pterm env) = sterm_to_pterm (subst t env)" proof (induction t arbitrary: env rule: sterm_induct) case (Sabs cs) show ?case apply simp apply (rule fset.map_cong0) apply (auto split: prod.splits) apply (rule Sabs) by (auto simp: fset_of_list.rep_eq) qed (auto split: option.splits) instantiation pterm :: "term" begin definition abs_pred_pterm :: "(pterm bool) pterm bool" where [code del]: "abs_pred P t (cs. t = Pabs cs (pat t. (pat, t) |∈| cs P t) P t)" context begin private lemma abs_pred_trivI0: "P t abs_pred P (t::pterm)" unfolding abs_pred_pterm_def by auto instance proof (standard, goal_cases) case (1 P t) then show ?case by (induction t rule: pterm_induct) (auto simp: const_pterm_def free_pterm_def app_pterm_def abs_pred_pterm_def) next (* FIXME proving 2, 3 and 4 via sterm probably requires lifting setup *) (* lifting setup requires a consistent ordering without assumptions! *) (* but: other parts (in Eq_Logic_PM_Seq) require a key-ordering that only works with assumptions *) (* solution: don't try to abstract over the ordering *) case (2 t) show ?case unfolding abs_pred_pterm_def apply clarify apply (rule subst_pabs_id) by blast next case (3 x t) show ?case unfolding abs_pred_pterm_def apply clarsimp apply (rule fset.map_cong0) apply (rename_tac c) apply (case_tac c; hypsubst_thin) apply simp subgoal for cs env pat rhs apply (cases "x |∈| frees pat") subgoal apply (rule arg_cong[where f = "subst rhs"]) by (auto intro: fmap_ext) subgoal premises prems[rule_format] apply (subst (2) prems(1)[symmetric, where pat = pat]) subgoal by (subst fmember.rep_eq) fact subgoal using prems unfolding ffUnion_alt_def by (auto simp: fmember.rep_eq fset_of_list.rep_eq elim!: fBallE) subgoal apply (rule arg_cong[where f = "subst rhs"]) by (auto intro: fmap_ext) done done done next case (4 t) show ?case unfolding abs_pred_pterm_def apply clarsimp apply (rule fset.map_cong0) apply clarsimp subgoal premises prems[rule_format] for cs env1 env2 a b apply (rule prems(2)[unfolded fmember.rep_eq, OF prems(5)]) using prems unfolding fdisjnt_alt_def by auto done next case 5 show ?case proof (rule abs_pred_trivI0, clarify) fix t :: pterm fix env :: "(name, pterm) fmap" obtain t' where "t = sterm_to_pterm t'" by (rule sterm_to_pterm_total) obtain env' where "env = fmmap sterm_to_pterm env'" by (metis fmmap_total sterm_to_pterm_total) show "frees (subst t env) = frees t - fmdom env" if "fmpred (λ_. closed) env" unfolding t = _ env = _ apply simp apply (subst subst_sterm_to_pterm) apply simp apply (rule subst_frees) using that unfolding env = _ apply simp apply (rule fmpred_mono_strong; assumption?) unfolding closed_except_def by simp qed next case 6 show ?case proof (rule abs_pred_trivI0, clarify) fix t :: pterm fix env :: "(name, pterm) fmap" obtain t' where "t = sterm_to_pterm t'" by (rule sterm_to_pterm_total) obtain env' where "env = fmmap sterm_to_pterm env'" by (metis fmmap_total sterm_to_pterm_total) show "consts (subst t env) = consts t |∪| ffUnion (consts || fmimage env (frees t))" unfolding t = _ env = _ apply simp apply (subst comp_def) apply simp apply (subst subst_sterm_to_pterm) apply simp apply (rule subst_consts') done qed qed (rule abs_pred_trivI0) end end lemma no_abs_abs[simp]: "¬ no_abs (Pabs cs)" by (subst no_abs.simps) (auto simp: term_cases_def) lemma sterm_to_pterm: assumes "no_abs t" shows "sterm_to_pterm t = convert_term t" using assms proof induction case (free name) show ?case apply simp apply (simp add: free_sterm_def free_pterm_def) done next case (const name) show ?case apply simp apply (simp add: const_sterm_def const_pterm_def) done next case (app t1 t2) then show ?case apply simp apply (simp add: app_sterm_def app_pterm_def) done qed abbreviation Pabs_single ("Λp _. _" [0, 50] 50) where "Pabs_single x rhs Pabs {| (Free x, rhs) |}" lemma closed_except_simps: "closed_except (Pvar x) S x |∈| S" "closed_except (t1 p t2) S closed_except t1 S closed_except t2 S" "closed_except (Pabs cs) S fBall cs (λ(pat, t). closed_except t (S |∪| frees pat))" "closed_except (Pconst name) S True" proof goal_cases case 3 show ?case proof (standard, goal_cases) case 1 then show ?case apply (auto simp: ffUnion_alt_def closed_except_def) apply (drule ffUnion_least_rev) apply auto by (smt case_prod_conv fBall_alt_def fminus_iff fset_rev_mp id_apply map_prod_simp) next case 2 then show ?case by (fastforce simp: ffUnion_alt_def closed_except_def) qed qed (auto simp: ffUnion_alt_def closed_except_def) instantiation pterm :: pre_strong_term begin function (sequential) wellformed_pterm :: "pterm bool" where "wellformed_pterm (t1 p t2) wellformed_pterm t1 wellformed_pterm t2" | "wellformed_pterm (Pabs cs) fBall cs (λ(pat, t). linear pat wellformed_pterm t) is_fmap cs pattern_compatibles cs cs {||}" | "wellformed_pterm _ True" by pat_completeness auto termination proof (relation "measure size", goal_cases) case 4 then show ?case apply auto including fset.lifting apply transfer apply (rule le_imp_less_Suc) apply (rule sum_nat_le_single[where y = "(a, (b, size b))" for a b]) by auto qed auto primrec all_frees_pterm :: "pterm name fset" where "all_frees_pterm (Pvar x) = {|x|}" | "all_frees_pterm (t1 p t2) = all_frees_pterm t1 |∪| all_frees_pterm t2" | "all_frees_pterm (Pabs cs) = ffUnion ((λ(P, T). P |∪| T) || map_prod frees all_frees_pterm |`| cs)" | "all_frees_pterm (Pconst _) = {||}" instance by standard (auto simp: const_pterm_def free_pterm_def app_pterm_def) end lemma sterm_to_pterm_all_frees[simp]: "all_frees (sterm_to_pterm t) = all_frees t" proof (induction t) case (Sabs cs) show ?case apply simp apply (rule arg_cong[where f = ffUnion]) apply (rule fimage_cong[OF refl]) apply clarsimp apply (subst Sabs) by (auto simp: fset_of_list_elem snds.simps) qed auto instance pterm :: strong_term proof (standard, goal_cases) case (1 t) obtain t' where "t = sterm_to_pterm t'" by (metis sterm_to_pterm_total) show ?case apply (rule abs_pred_trivI) unfolding t = _ sterm_to_pterm_all_frees sterm_to_pterm_frees by (rule frees_all_frees) next case (2 t) show ?case unfolding abs_pred_pterm_def apply (intro allI impI) apply (simp add: case_prod_twice, intro conjI) subgoal by blast subgoal by (auto intro: is_fmap_image) subgoal unfolding fpairwise_image fpairwise_alt_def by (auto elim!: fBallE) done qed lemma wellformed_PabsI: assumes "is_fmap cs" "pattern_compatibles cs" "cs {||}" assumes "pat t. (pat, t) |∈| cs linear pat" assumes "pat t. (pat, t) |∈| cs wellformed t" shows "wellformed (Pabs cs)" using assms by auto corollary subst_closed_pabs: assumes "(pat, rhs) |∈| cs" "closed (Pabs cs)" shows "subst rhs (fmdrop_fset (frees pat) env) = rhs" using assms by (subst subst_closed_except_id) (auto simp: fdisjnt_alt_def closed_except_simps) lemma (in constants) shadows_consts_pterm_simps[simp]: "shadows_consts (t1 p t2) shadows_consts t1 shadows_consts t2" "shadows_consts (Pvar name) name |∈| all_consts" "shadows_consts (Pabs cs) fBex cs (λ(pat, t). shadows_consts pat shadows_consts t)" "shadows_consts (Pconst name) False" proof goal_cases case 3 (* FIXME duplicated from Sterm *) show ?case unfolding shadows_consts_def apply rule subgoal by (force simp: ffUnion_alt_def fset_of_list_elem fdisjnt_alt_def elim!: ballE) subgoal apply (auto simp: fset_of_list_elem fdisjnt_alt_def) by (auto simp: fset_eq_empty_iff ffUnion_alt_def fset_of_list_elem elim!: allE fBallE) done qed (auto simp: shadows_consts_def fdisjnt_alt_def) end # Theory Term_as_Value section ‹Irreducible terms (values)› theory Term_as_Value imports Sterm begin section ‹Viewing @{typ sterm} as values› (* FIXME why isn't this declared by BNF *) declare list.pred_mono[mono] context constructors begin inductive is_value :: "sterm bool" where abs: "is_value (Sabs cs)" | constr: "list_all is_value vs name |∈| C is_value (name$$ vs)" lemma value_distinct: "Sabs cs name $$ts" (is ?P) "name$$ ts Sabs cs" (is ?Q) proof - show ?P apply (rule list_comb_cases'[where f = "const name" and xs = ts]) apply (auto simp: const_sterm_def is_app_def elim: unapp_sterm.elims) done thus ?Q by simp qed abbreviation value_env :: "(name, sterm) fmap bool" where "value_env fmpred (λ_. is_value)" lemma svar_value[simp]: "¬ is_value (Svar name)" proof assume "is_value (Svar name)" thus False apply (cases rule: is_value.cases) apply (fold free_sterm_def) by simp qed lemma value_cases: obtains (comb) name vs where "list_all is_value vs" "t = name $$vs" "name |∈| C" | (abs) cs where "t = Sabs cs" | (nonvalue) "¬ is_value t" proof (cases t) case Svar thus thesis using nonvalue by simp next case Sabs thus thesis using abs by (auto intro: is_value.abs) next case (Sconst name) have "list_all is_value []" by simp have "t = name$$ []" unfolding Sconst by (simp add: const_sterm_def) show thesis using comb is_value.cases abs nonvalue by blast next case Sapp show thesis proof (cases "is_value t") case False thus thesis using nonvalue by simp next case True then obtain name vs where "list_all is_value vs" "t = name $$vs" "name |∈| C" unfolding Sapp by cases auto thus thesis using comb by simp qed qed end fun smatch' :: "pat sterm (name, sterm) fmap option" where "smatch' (Patvar name) t = Some (fmap_of_list [(name, t)])" | "smatch' (Patconstr name ps) t = (case strip_comb t of (Sconst name', vs) (if name = name' length ps = length vs then map_option (foldl (++f) fmempty) (those (map2 smatch' ps vs)) else None) | _ None)" lemmas smatch'_induct = smatch'.induct[case_names var constr] context constructors begin context begin private lemma smatch_list_comb_is_value: assumes "is_value t" shows "match (name$$ ps) t = (case strip_comb t of (Sconst name', vs) (if name = name' length ps = length vs then map_option (foldl (++f) fmempty) (those (map2 match ps vs)) else None) | _ None)" using assms apply cases apply (auto simp: strip_list_comb split: option.splits) apply (subst (2) const_sterm_def) apply (auto simp: matchs_alt_def) done lemma smatch_smatch'_eq: assumes "linear pat" "is_value t" shows "match pat t = smatch' (mk_pat pat) t" using assms proof (induction pat arbitrary: t rule: linear_pat_induct) case (comb name args) show ?case using ‹is_value t proof (cases rule: is_value.cases) case (abs cs) thus ?thesis by (force simp: strip_list_comb_const) next case (constr args' name') have "map2 match args args' = map2 smatch' (map mk_pat args) args'" if "length args = length args'" using that constr(2) comb(2) by (induct args args' rule: list_induct2) auto thus ?thesis using constr apply (auto simp: smatch_list_comb_is_value strip_list_comb map_option_case strip_list_comb_const intro: is_value.intros) apply (subst (2) const_sterm_def) apply (auto simp: matchs_alt_def) done qed qed simp end end end # Theory Value section ‹A dedicated value type› theory Value imports Term_as_Value begin datatype "value" = is_Vconstr: Vconstr name "value list" | Vabs "sclauses" "(name, value) fmap" | Vrecabs "(name, sclauses) fmap" name "(name, value) fmap" type_synonym vrule = "name × value" setup ‹Sign.mandatory_path "quickcheck" (* FIXME: make private, prevented by bug in datatype_compat; workaround: mandatory path *) datatype "value" = Vconstr name "value list" | Vabs "sclauses" "(name × value) list" | Vrecabs "(name × sclauses) list" name "(name × value) list" primrec "Value" :: "quickcheck.value value" where "Value (quickcheck.Vconstr s vs) = Vconstr s (map Value vs)" | "Value (quickcheck.Vabs cs Γ) = Vabs cs (fmap_of_list (map (map_prod id Value) Γ))" | "Value (quickcheck.Vrecabs css name Γ) = Vrecabs (fmap_of_list css) name (fmap_of_list (map (map_prod id Value) Γ))" setup ‹Sign.parent_path› quickcheck_generator "value" constructors: quickcheck.Value fun vmatch :: "pat value (name, value) fmap option" where "vmatch (Patvar name) v = Some (fmap_of_list [(name, v)])" | "vmatch (Patconstr name ps) (Vconstr name' vs) = (if name = name' length ps = length vs then map_option (foldl (++f) fmempty) (those (map2 vmatch ps vs)) else None)" | "vmatch _ _ = None" lemmas vmatch_induct = vmatch.induct[case_names var constr] locale value_pred = fixes P :: "(name, value) fmap sclauses bool" fixes Q :: "name bool" fixes R :: "name fset bool" begin primrec pred :: "value bool" where "pred (Vconstr name vs) Q name list_all id (map pred vs)" | "pred (Vabs cs Γ) pred_fmap id (fmmap pred Γ) P Γ cs" | "pred (Vrecabs css name Γ) pred_fmap id (fmmap pred Γ) pred_fmap (P Γ) css name |∈| fmdom css R (fmdom css)" declare pred.simps[simp del] lemma pred_alt_def[simp, code]: "pred (Vconstr name vs) Q name list_all pred vs" "pred (Vabs cs Γ) fmpred (λ_. pred) Γ P Γ cs" "pred (Vrecabs css name Γ) fmpred (λ_. pred) Γ pred_fmap (P Γ) css name |∈| fmdom css R (fmdom css)" by (auto simp: list_all_iff pred.simps) text ‹ For technical reasons, we don't introduce an abbreviation for @{prop ‹fmpred (λ_. pred) env} here. This locale is supposed to be interpreted with @{command global_interpretation} (or @{command sublocale} and a @{theory_text defines} clause. However, this does not affect abbreviations: the abbreviation would still refer to the locale constant, not the constant introduced by the interpretation. › lemma vmatch_env: assumes "vmatch pat v = Some env" "pred v" shows "fmpred (λ_. pred) env" using assms proof (induction pat v arbitrary: env rule: vmatch_induct) case (constr name ps name' vs) hence "map_option (foldl (++f) fmempty) (those (map2 vmatch ps vs)) = Some env" "name = name'" "length ps = length vs" by (auto split: if_splits) then obtain envs where "env = foldl (++f) fmempty envs" "map2 vmatch ps vs = map Some envs" by (blast dest: those_someD) moreover have "fmpred (λ_. pred) env" if "env set envs" for env proof - from that have "Some env set (map2 vmatch ps vs)" unfolding ‹map2 _ _ _ = _ by simp then obtain p v where "p set ps" "v set vs" "vmatch p v = Some env" apply (rule map2_elemE) by auto hence "pred v" using constr by (simp add: list_all_iff) show ?thesis by (rule constr; safe?) fact+ qed ultimately show ?case by auto qed auto end primrec value_to_sterm :: "value sterm" where "value_to_sterm (Vconstr name vs) = name$\$ map value_to_sterm vs" |
"value_to_sterm (Vabs cs Γ) = Sabs (map (λ(pat, t). (pat, subst t (fmdrop_fset (frees pat) (fmmap value_to_sterm Γ)))) cs)" |
"value_to_sterm (Vrecabs css name Γ) =
Sabs (map (λ(pat, t). (pat, subst t (fmdrop_fset (frees pat) (fmmap value_to_sterm Γ)))) (the (fmlookup css name)))"

text ‹
This locale establishes a connection between a predicate on @{typ value}s with the corresponding
predicate on @{typ sterm}s, by means of @{const value_to_sterm}.
›

locale pre_value_sterm_pred = value_pred +
fixes S
assumes value_to_sterm: "pred v  S (value_to_sterm v)"
begin

corollary value_to_sterm_env:
assumes "fmpred (λ_. pred) Γ"
shows "fmpred (λ_. S) (fmmap value_to_sterm Γ)"
unfolding fmpred_map proof
fix name v
assume "fmlookup Γ name = Some v"
with assms have "pred v" by (metis fmpredD)
thus "S (value_to_sterm v)" by (rule value_to_sterm)
qed

end

locale value_sterm_pred = value_pred + S: simple_syntactic_and S for S +
assumes const: "name. Q name  S (const name)"
assumes abs: "Γ cs.
(n v. fmlookup Γ n = Some v  pred v  S (value_to_sterm v))
fmpred (λ_. pred) Γ
P Γ cs
S (Sabs (map (λ(pat, t). (pat, subst t (fmmap value_to_sterm (fmdrop_fset (frees pat) Γ)))) cs))"
begin

sublocale pre_value_sterm_pred
proof
fix v
assume "pred v"
then show "S (value_to_sterm v)"
proof (induction v)
case (Vconstr x1 x2)
show ?case
apply simp
unfolding S.list_comb
apply rule
apply (rule const)
using Vconstr by (auto simp: list_all_iff)
next
case (Vabs x1 x2)
show ?case
apply auto
apply (rule abs)
using Vabs
by (auto intro: fmran'I)
next
case (Vrecabs x1 x2 x3)
show ?case
apply auto
apply (rule abs)
using Vrecabs
by (auto simp: fmlookup_dom_iff fmpred_iff intro: fmran'I)
qed
qed

end

global_interpretation vwellformed:
value_sterm_pred
"λ_. wellformed_clauses"
"λ_. True"
"λ_. True"
wellformed
defines vwellformed = vwellformed.pred
proof (standard, goal_cases)
case (2 Γ cs)
hence "cs  []"
by simp

moreover have "wellformed (subst rhs (fmdrop_fset (frees pat) (fmmap value_to_sterm Γ)))"
if "(pat, rhs)  set cs" for pat rhs
proof -
show ?thesis
apply (rule subst_wellformed)
subgoal using 2 that by (force simp: list_all_iff)
apply (rule fmpred_drop_fset)
using 2 by auto
qed

moreover have "distinct (map (fst  (λ(pat, t). (pat, subst t (fmmap value_to_sterm (fmdrop_fset (frees pat) Γ))))) cs)"
apply (subst map_cong[OF refl, where g = fst])
using 2 by auto

ultimately show ?case
using 2 by (auto simp: list_all_iff)
qed (auto simp: const_sterm_def)

abbreviation "wellformed_venv  fmpred (λ_. vwellformed)"

global_interpretation vclosed:
value_sterm_pred
"λΓ cs. list_all (λ(pat, t). closed_except t (fmdom Γ |∪| frees pat)) cs"
"λ_. True"
"λ_. True"
closed
defines vclosed = vclosed.pred
proof (standard, goal_cases)
case (2 Γ cs)
show ?case
apply (simp add: list_all_iff case_prod_twice Sterm.closed_except_simps)
apply safe
apply (subst closed_except_def)
apply (subst subst_frees)
apply simp
subgoal
apply (rule fmpred_drop_fset)
apply (rule fmpredI)
apply (rule 2)
apply assumption
using 2 by auto
subgoal
using 2 by (auto simp: list_all_iff closed_except_def)
done
qed simp

abbreviation "closed_venv  fmpred (λ_. vclosed)"

context pre_constants begin

sublocale vwelldefined:
value_sterm_pred
"λ_ cs. list_all (λ(_, t). welldefined t) cs"
"λname. name |∈| C"
welldefined
defines vwelldefined = vwelldefined.pred
proof (standard, goal_cases)
case (2 Γ cs)
note fset_of_list_map[simp del]

show ?case
apply simp
apply (rule ffUnion_least)
apply (rule fBallI)
apply (subst (asm) fset_of_list_elem)
apply simp
apply (erule imageE)
subgoal for _ x
apply (cases x)
apply simp
apply (rule subst_consts)
subgoal
using 2 by (fastforce simp: list_all_iff)
subgoal
apply simp
apply (rule fmpred_drop_fset)
unfolding fmpred_map
apply (rule fmpredI)
using 2 by auto
done
done

lemmas vwelldefined_alt_def = vwelldefined.pred_alt_def

end

declare pre_constants.vwelldefined_alt_def[code]

context constructors begin

sublocale vconstructor_value:
pre_value_sterm_pred
"λ_ _. True"
"λname. name |∈| C"
"λ_. True"
is_value
defines vconstructor_value = vconstructor_value.pred
proof
fix v
assume "value_pred.pred (λ_ _. True) (λname. name |∈| C) (λ_. True) v"
then show "is_value (value_to_sterm v)"
proof (induction v)
case (Vconstr name vs)
hence "list_all is_value (map value_to_sterm vs)"
by (fastforce simp: list_all_iff value_pred.pred_alt_def)
show ?case
unfolding value_to_sterm.simps
apply (rule is_value.constr)
apply fact
using Vconstr by (simp add: value_pred.pred_alt_def)
qed (auto simp: disjnt_def intro: is_value.intros)
qed

lemmas vconstructor_value_alt_def = vconstructor_value.pred_alt_def

abbreviation "vconstructor_value_env  fmpred (λ_. vconstructor_value)"

definition vconstructor_value_rs :: "vrule list  bool" where
"vconstructor_value_rs rs
list_all (λ(_, rhs). vconstructor_value rhs) rs
fdisjnt (fset_of_list (map fst rs)) C"

end

declare constructors.vconstructor_value_alt_def[code]
declare constructors.vconstructor_value_rs_def[code]

context pre_constants begin

value_sterm_pred
"λ_ cs. list_all (λ(pat, t). fdisjnt all_consts (frees pat)  ¬ shadows_consts t) cs"
"λ_. True"
"λ_. True"
proof (standard, goal_cases)
case (2 Γ cs)
show ?case
apply (simp add: list_all_iff list_ex_iff case_prod_twice)
apply (rule ballI)
subgoal for x
apply (cases x, simp)
apply (rule conjI)
subgoal
using 2 by (force simp: list_all_iff)
subgoal
using 2 by (force simp: list_all_iff)
apply simp
apply (rule fmpred_drop_fset)
apply (rule fmpredI)
using 2 by auto
done
qed (auto simp: const_sterm_def app_sterm_def)

end

fun term_to_value :: "sterm  value" where
"term_to_value t =
(case strip_comb t of
(Sconst name, args)  Vconstr name (map term_to_value args)
| (Sabs cs, [])  Vabs cs fmempty)"

lemma (in constructors) term_to_value_to_sterm:
assumes "is_value t"
shows "value_to_sterm (term_to_value t) = t"
using assms proof induction
case (constr vs name)

have "map (value_to_sterm  term_to_value) vs = map id vs"
proof (rule list.map_cong0, unfold comp_apply id_apply)
fix v
assume "v  set vs"
with constr show "value_to_sterm (term_to_value v) = v"
qed
thus ?case
apply (subst const_sterm_def)
by simp
qed simp

lemma vmatch_dom:
assumes "vmatch pat v = Some env"
shows "fmdom env = patvars pat"
using assms proof (induction pat v arbitrary: env rule: vmatch_induct)
case (constr name ps name' vs)
hence
"map_option (foldl (++f) fmempty) (those (map2 vmatch ps vs)) = Some env"
"name = name'" "length ps = length vs"
by (auto split: if_splits)
then obtain envs where "env = foldl (++f) fmempty envs" "map2 vmatch ps vs = map Some envs"
by (blast dest: those_someD)

moreover have "fset_of_list (map fmdom envs) = fset_of_list (map patvars ps)"
proof safe
fix names
assume "names |∈| fset_of_list (map fmdom envs)"
hence "names  set (map fmdom envs)"
unfolding fset_of_list_elem .
then obtain env where "env  set envs" "names = fmdom env"
by auto
hence "Some env  set (map2 vmatch ps vs)"
unfolding ‹map2 _ _ _ = _ by simp
then obtain p v where "p  set ps" "v  set vs" "vmatch p v = Some env"
by (auto elim: map2_elemE)
moreover hence "fmdom env = patvars p"
using constr by fastforce
ultimately have "names  set (map patvars ps)"
unfolding names = _ by simp
thus "names |∈| fset_of_list (map patvars ps)"
unfolding fset_of_list_elem .
next
fix names
assume "names |∈| fset_of_list (map patvars ps)"
hence "names  set (map patvars ps)"
unfolding fset_of_list_elem .
then obtain p where "p  set ps" "names = patvars p"
by auto
then obtain v where "v  set vs" "vmatch p v  set (map2 vmatch ps vs)"
using ‹length ps = length vs by (auto elim!: map2_elemE1)
then obtain env where "env  set envs" "vmatch p v = Some env"
unfolding ‹map2 vmatch ps vs = _ by auto
moreover hence "fmdom env = patvars p"
using constr name = name' ‹length ps = length vs p  set ps v  set vs
by fastforce
ultimately have "names  set (map fmdom envs)"
unfolding names = _ by auto
thus "names |∈| fset_of_list (map fmdom envs)"
unfolding fset_of_list_elem .
qed

ultimately show ?case
qed auto

fun vfind_match :: "sclauses  value  ((name, value) fmap × term × sterm) option" where
"vfind_match [] _ = None" |
"vfind_match ((pat, rhs) # cs) t =
(case vmatch (mk_pat pat) t of
Some env  Some (env, pat, rhs)
| None  vfind_match cs t)"

lemma vfind_match_elem:
assumes "vfind_match cs t = Some (env, pat, rhs)"
shows "(pat, rhs)  set cs" "vmatch (mk_pat pat) t = Some env"
using assms
by (induct cs) (auto split: option.splits)

inductive veq_structure :: "value  value  bool" where
abs_abs: "veq_structure (Vabs _ _) (Vabs _ _)" |
recabs_recabs: "veq_structure (Vrecabs _ _ _) (Vrecabs _ _ _)" |
constr_constr: "list_all2 veq_structure ts us  veq_structure (Vconstr name ts) (Vconstr name us)"

lemma veq_structure_simps[code, simp]:
"veq_structure (Vabs cs1 Γ1) (Vabs cs2 Γ2)"
"veq_structure (Vrecabs css1 name1 Γ1) (Vrecabs css2 name2 Γ2)"
"veq_structure (Vconstr name1 ts) (Vconstr name2 us)  name1 = name2  list_all2 veq_structure ts us"
by (auto intro: veq_structure.intros elim: veq_structure.cases)

lemma veq_structure_refl[simp]: "veq_structure t t"
by (induction t) (auto simp: list.rel_refl_strong)

global_interpretation vno_abs: value_pred "λ_ _. False" "λ_. True" "λ_. False"
defines vno_abs = vno_abs.pred .

lemma veq_structure_eq_left:
assumes "veq_structure t u" "vno_abs t"
shows "t = u"
using assms proof (induction rule: veq_structure.induct)
case (constr_constr ts us name)
have "ts = us" if "list_all vno_abs ts"
using constr_constr.IH that
by induction auto
with constr_constr show ?case
by auto
qed auto

lemma veq_structure_eq_right:
assumes "veq_structure t u" "vno_abs u"
shows "t = u"
using assms proof (induction rule: veq_structure.induct)
case (constr_constr ts us name)
have "ts = us" if "list_all vno_abs us"
using constr_constr.IH that
by induction auto
with constr_constr show ?case
by auto
qed auto

fun vmatch' :: "pat  value  (name, value) fmap option" where
"vmatch' (Patvar name) v = Some (fmap_of_list [(name, v)])" |
"vmatch' (Patconstr name ps) v =
(case v of
Vconstr name' vs
(if name = name'  length ps = length vs then
map_option (foldl (++f) fmempty) (those (map2 vmatch' ps vs))
else
None)
| _  None)"

lemma vmatch_vmatch'_eq: "vmatch p v = vmatch' p v"
proof (induction rule: vmatch.induct)
case (2 name ps name' vs)
then show ?case
apply auto
apply (rule map_option_cong[OF _ refl])
apply (rule arg_cong[where f = those])
apply (rule map2_cong[OF refl refl])
apply blast
done
qed auto

locale value_struct_rel =
fixes Q :: "value  value  bool"
assumes Q_impl_struct: "Q t1 t2  veq_structure t1 t2"
assumes Q_def[simp]: "Q (Vconstr name ts) (Vconstr name' us)  name = name'  list_all2 Q ts us"
begin

lemma eq_left: "Q t u  vno_abs t  t = u"
using Q_impl_struct by (metis veq_structure_eq_left)

lemma eq_right: "Q t u  vno_abs u  t = u"
using Q_impl_struct by (metis veq_structure_eq_right)

context begin

private lemma vmatch'_rel:
assumes "Q t1 t2"
shows "rel_option (fmrel Q) (vmatch' p t1) (vmatch' p t2)"
using assms(1) proof (induction p arbitrary: t1 t2)
case (Patconstr name ps)
with Q_impl_struct have "veq_structure t1 t2"
by blast

thus ?case
proof (cases rule: veq_structure.cases)
case (constr_constr ts us name')

{
assume "length ps = length ts"

have "list_all2 (rel_option (fmrel Q)) (map2 vmatch' ps ts) (map2 vmatch' ps us)"
using ‹list_all2 veq_structure ts us Patconstr ‹length ps = length ts
unfolding t1 = _ t2 = _
proof (induction arbitrary: ps)
case (Cons t ts u us ps0)
then obtain p ps where "ps0 = p # ps"
by (cases ps0) auto

have "length ts = length us"
using Cons by (auto dest: list_all2_lengthD)

hence "Q t u"
using Q (Vconstr name' (t # ts)) (Vconstr name' (u # us))
hence "rel_option (fmrel Q) (vmatch' p t) (vmatch' p u)"
using Cons unfolding ps0 = _ by simp

moreover have "list_all2 (rel_option (fmrel Q)) (map2 vmatch' ps ts) (map2 vmatch' ps us)"
apply (rule Cons)
subgoal
apply (rule Cons)
unfolding ps0 = _ apply simp
by assumption
subgoal
using Q (Vconstr name' (t # ts)) (Vconstr name' (u # us)) ‹length ts = length us
subgoal
using ‹length ps0 = length (t # ts)
unfolding ps0 = _ by simp
done

ultimately show ?case
unfolding ps0 = _
by auto
qed auto

hence "rel_option (list_all2 (fmrel Q)) (those (map2 vmatch' ps ts)) (those (map2 vmatch' ps us))"
by (rule rel_funD[OF those_transfer])

have
"rel_option (fmrel Q)
(map_option (foldl (++f) fmempty) (those (map2 vmatch' ps ts)))
(map_option (foldl (++f) fmempty) (those (map2 vmatch' ps us)))"
apply (rule rel_funD[OF rel_funD[OF option.map_transfer]])
apply transfer_prover
by fact
}
note * = this

have "length ts = length us"
using constr_constr by (auto dest: list_all2_lengthD)

thus ?thesis
unfolding t1 = _ t2 = _
apply auto
apply (rule *)
by simp
qed auto
qed auto

lemma vmatch_rel: "Q t1 t2  rel_option (fmrel Q) (vmatch p t1) (vmatch p t2)"
unfolding vmatch_vmatch'_eq by (rule vmatch'_rel)

lemma vfind_match_rel:
assumes "list_all2 (rel_prod (=) R) cs1 cs2"
assumes "Q t1 t2"
shows "rel_option (rel_prod (fmrel Q) (rel_prod (=) R)) (vfind_match cs1 t1) (vfind_match cs2 t2)"
using assms(1) proof induction
case (Cons c1 cs1 c2 cs2)
moreover obtain pat1 rhs1 where "c1 = (pat1, rhs1)" by fastforce
moreover obtain pat2 rhs2 where "c2 = (pat2, rhs2)" by fastforce

ultimately have "pat1 = pat2" "R rhs1 rhs2"
by auto

have "rel_option (fmrel Q) (vmatch (mk_pat pat1) t1) (vmatch (mk_pat pat1) t2)"
by (rule vmatch_rel) fact
thus ?case
proof cases
case None
thus ?thesis
unfolding c1 = _ c2 = _ pat1 = _
using Cons by auto
next
case (Some Γ1 Γ2)
thus ?thesis
unfolding c1 = _ c2 = _ pat1 = _
using R rhs1 rhs2
by auto
qed
qed simp

lemmas vfind_match_rel' =
vfind_match_rel[
where R = "(=)" and cs1 = cs and cs2 = cs for cs,
unfolded prod.rel_eq,
OF list.rel_refl, OF refl]

end end

hide_fact vmatch_vmatch'_eq
hide_const vmatch'

global_interpretation veq_structure: value_struct_rel veq_structure
by standard auto

abbreviation env_eq where
"env_eq  fmrel (λv t. t = value_to_sterm v)"

lemma env_eq_eq:
assumes "env_eq venv senv"
shows "senv = fmmap value_to_sterm venv"
proof (rule fmap_ext, unfold fmlookup_map)
fix name
from assms have "rel_option (λv t. t = value_to_sterm v) (fmlookup venv name) (fmlookup senv name)"
by auto
thus "fmlookup senv name = map_option value_to_sterm (fmlookup venv name)"
by cases auto
qed

context constructors begin

context begin

private lemma vmatch_eq0: "rel_option env_eq (vmatch p v) (smatch' p (value_to_sterm v))"
proof (induction p v rule: vmatch_induct)
case (constr name ps name' vs)

have
"rel_option env_eq
(map_option (foldl (++f) Γ) (those (map2 vmatch ps vs)))
(map_option (foldl (++f) Γ') (those (map2 smatch' ps (map value_to_sterm vs))))"
if "length ps = length vs" and "name = name'" and "env_eq Γ Γ'" for Γ Γ'
using that constr
proof (induction arbitrary: Γ Γ' rule: list_induct2)
case (Cons p ps v vs)
hence "rel_option env_eq (vmatch p v) (smatch' p (value_to_sterm v))"
by auto
thus ?case
proof cases
case (Some Γ1 Γ2)
thus ?thesis
apply (rule Cons)
using Cons by auto
qed simp
qed fastforce

thus ?case
apply (auto simp: strip_list_comb_const)
apply (subst const_sterm_def, simp)+
done
qed auto

corollary vmatch_eq:
assumes "linear p" "vconstructor_value v"
shows "rel_option env_eq (vmatch (mk_pat p) v) (match p (value_to_sterm v))"
using assms
by (metis smatch_smatch'_eq vmatch_eq0 vconstructor_value.value_to_sterm)

end

end

abbreviation match_related where
"match_related  (λ(Γ1, pat1, rhs1) (Γ2, pat2, rhs2). rhs1 = rhs2  pat1 = pat2  env_eq Γ1 Γ2)"

lemma (in constructors) find_match_eq:
assumes "list_all (linear  fst) cs" "vconstructor_value v"
shows "rel_option match_related (vfind_match cs v) (find_match cs (value_to_sterm v))"
using assms proof (induct cs)
case (Cons c cs)
then obtain p t where "c = (p, t)" by fastforce
hence "rel_option env_eq (vmatch (mk_pat p) v) (match p (value_to_sterm v))"
using Cons by (fastforce intro: vmatch_eq)
thus ?case
using Cons unfolding c = _
by cases auto
qed auto

inductive erelated :: "value  value  bool" ("_ e _") where
constr: "list_all2 erelated ts us  Vconstr name ts e Vconstr name us" |
abs: "fmrel_on_fset (ids (Sabs cs)) erelated Γ1 Γ2  Vabs cs Γ1 e Vabs cs Γ2" |
rec_abs:
"pred_fmap (λcs. fmrel_on_fset (ids (Sabs cs)) erelated Γ1 Γ2) css
Vrecabs css name Γ1 e Vrecabs css name Γ2"

code_pred erelated .

global_interpretation erelated: value_struct_rel erelated
proof
fix v1 v2
assume "v1 e v2"
thus "veq_structure v1 v2"
by induction (auto intro: list.rel_mono_strong)
next
fix name name' and ts us :: "value list"
show "Vconstr name ts e Vconstr name' us  (name = name'  list_all2 erelated ts us)"
by (auto intro: erelated.intros elim: erelated.cases)
qed

lemma erelated_refl[intro]: "t e t"
proof (induction t)
case Vrecabs
thus ?case
apply (auto intro!: erelated.intros fmpredI fmrel_on_fset_refl_strong)
apply (auto intro: fmran'I)
done
qed (auto intro!: erelated.intros list.rel_refl_strong fmrel_on_fset_refl_strong fmran'I)

export_code
value_to_sterm vmatch vwellformed vclosed erelated_i_i pre_constants.vwelldefined
vfind_match veq_structure vno_abs
checking Scala

end

# Theory Doc_CupCake

chapter ‹A smaller version of CakeML: CupCakeML›

theory Doc_CupCake
imports Main
begin

end

# Theory CupCake_Env

section ‹CupCake environments›

theory CupCake_Env
imports
begin

fun cake_no_abs :: "v  bool" where
"cake_no_abs (Conv _ vs)  list_all cake_no_abs vs" |
"cake_no_abs _  False"

fun is_cupcake_pat :: "Ast.pat  bool" where
"is_cupcake_pat (Ast.Pvar _)  True" |
"is_cupcake_pat (Ast.Pcon (Some (Short _)) xs)  list_all is_cupcake_pat xs" |
"is_cupcake_pat _  False"

fun is_cupcake_exp :: "exp  bool" where
"is_cupcake_exp (Ast.Var (Short _))  True" |
"is_cupcake_exp (Ast.App oper es)  oper = Ast.Opapp  list_all is_cupcake_exp es" |
"is_cupcake_exp (Ast.Con (Some (Short _)) es)  list_all is_cupcake_exp es" |
"is_cupcake_exp (Ast.Fun _ e)  is_cupcake_exp e" |
"is_cupcake_exp (Ast.Mat e cs)  is_cupcake_exp e  list_all (λ(p, e). is_cupcake_pat p  is_cupcake_exp e) cs  cake_linear_clauses cs" |
"is_cupcake_exp _  False"

abbreviation cupcake_clauses :: "(Ast.pat × exp) list  bool" where
"cupcake_clauses  list_all (λ(p, e). is_cupcake_pat p  is_cupcake_exp e)"

fun cupcake_c_ns :: "c_ns  bool" where
"cupcake_c_ns (Bind cs mods)
mods = []  list_all (λ(_, _, tid). case tid of TypeId (Short _)  True | _  False) cs"

locale cakeml_static_env =
fixes static_cenv :: c_ns
assumes static_cenv: "cupcake_c_ns static_cenv"
begin

definition empty_sem_env :: "v sem_env" where
"empty_sem_env =  sem_env.v = nsEmpty, sem_env.c = static_cenv "

lemma v_of_empty_sem_env[simp]: "sem_env.v empty_sem_env = nsEmpty"
unfolding empty_sem_env_def by simp

lemma c_of_empty_sem_env[simp]: "c empty_sem_env = static_cenv"
unfolding empty_sem_env_def by simp

fun is_cupcake_value :: "SemanticPrimitives.v  bool"
and is_cupcake_all_env :: "all_env  bool" where
"is_cupcake_value (Conv (Some (_, TypeId (Short _))) vs)  list_all is_cupcake_value vs" |
"is_cupcake_value (Closure env _ e)  is_cupcake_exp e  is_cupcake_all_env env" |
"is_cupcake_value (Recclosure env es _)  list_all (λ(_, _, e). is_cupcake_exp e) es  is_cupcake_all_env env" |
"is_cupcake_value _  False" |
"is_cupcake_all_env  sem_env.v = Bind v0 [], sem_env.c = c0   c0 = static_cenv  list_all (is_cupcake_value  snd) v0" |
"is_cupcake_all_env _  False"

lemma is_cupcake_all_envE:
assumes "is_cupcake_all_env env"
obtains v c where "env =  sem_env.v = Bind v [], sem_env.c = c " "c = static_cenv" "list_all (is_cupcake_value  snd) v"
using assms
by (auto elim!: is_cupcake_all_env.elims)

fun is_cupcake_ns :: "v_ns  bool" where
"is_cupcake_ns (Bind v0 [])  list_all (is_cupcake_value  snd) v0" |
"is_cupcake_ns _  False"

lemma is_cupcake_nsE:
assumes "is_cupcake_ns ns"
obtains v where "ns = Bind v []" "list_all (is_cupcake_value  snd) v"
using assms by (rule is_cupcake_ns.elims)

lemma is_cupcake_all_envD:
assumes "is_cupcake_all_env env"
shows "is_cupcake_ns (sem_env.v env)" "cupcake_c_ns (c env)"
using assms static_cenv by (auto elim!: is_cupcake_all_envE)

lemma is_cupcake_all_envI:
assumes "is_cupcake_ns (sem_env.v env)" "sem_env.c env = static_cenv"
shows "is_cupcake_all_env env"
using assms static_cenv
apply (cases env)
apply simp
subgoal for v c
apply (cases v)
apply simp
subgoal for x1 x2
by (cases x2) auto
done
done

end

end

# Theory CupCake_Semantics

section ‹CupCake semantics›

theory CupCake_Semantics
imports
CupCake_Env
CakeML.Matching
CakeML.Big_Step_Unclocked_Single
begin

fun cupcake_nsLookup :: "('m,'n,'v)namespace  'n  'v option "  where
"cupcake_nsLookup (Bind v1 _) n = map_of v1 n"

lemma cupcake_nsLookup_eq[simp]: "nsLookup ns (Short n) = cupcake_nsLookup ns n"
by (cases ns) auto

fun cupcake_pmatch :: "((string),(string),(nat*tid_or_exn))namespace  pat  v (string*v)list ((string*v)list)match_result " where
"cupcake_pmatch cenv (Pvar x) v0 env = Match ((x, v0)# env)" |
"cupcake_pmatch cenv (Pcon (Some (Short n)) ps) (Conv (Some (n', t')) vs) env =
(case cupcake_nsLookup cenv n of
Some (l, t)=>
if same_tid t t'  (List.length ps = l) then
if same_ctor (n, t) (n',t') then
Matching.fold2 (λp v m. case m of
Match env  cupcake_pmatch cenv p v env
| m  m) Match_type_error ps vs (Match env)
else
No_match
else
Match_type_error
| _ => Match_type_error)" |
"cupcake_pmatch cenv _ _ _ = Match_type_error"

fun cupcake_match_result :: "_  v (pat*exp)list  v  (exp × pat × (char list × v) list, v)result" where
"cupcake_match_result _ _ [] err_v = Rerr (Rraise err_v)" |
"cupcake_match_result cenv v0 ((p, e) # pes) err_v =
(if distinct (pat_bindings p []) then
(case cupcake_pmatch cenv p v0 [] of
Match env'  Rval (e, p, env') |
No_match  cupcake_match_result cenv v0 pes err_v |
Match_type_error  Rerr (Rabort Rtype_error))
else
Rerr (Rabort Rtype_error))"

lemma cupcake_match_resultE:
assumes "cupcake_match_result cenv v0 pes err_v = Rval (e, p, env')"
obtains init rest
where "pes = init @ (p, e) # rest"
and "distinct (pat_bindings p [])"
and "list_all (λ(p, e). cupcake_pmatch cenv p v0 [] = No_match  distinct (pat_bindings p [])) init"
and "cupcake_pmatch cenv p v0 [] = Match env'"
using assms
proof (induction pes)
case (Cons pe pes)
obtain p0 e0 where "pe = (p0, e0)"
by fastforce

show thesis
proof (cases "distinct (pat_bindings p0 [])")
case True
thus ?thesis
proof (cases "cupcake_pmatch cenv p0 v0 []")
case No_match
show ?thesis
proof (rule Cons)
fix init rest
assume "pes = init @ (p, e) # rest"
assume "list_all (λ(p, e). cupcake_pmatch cenv p v0 [] = No_match  distinct (pat_bindings p [])) init"
assume "distinct (pat_bindings p [])"
assume "cupcake_pmatch cenv p v0 [] = Match env'"

moreover have "pe # pes = ((p0, e0) # init) @ (p, e) # rest"
unfolding pes = _ pe = _ by simp

moreover have "list_all (λ(p, e). cupcake_pmatch cenv p v0 [] = No_match  distinct (pat_bindings p [])) ((p0, e0) # init)"
apply auto
subgoal by fact
subgoal using True by simp
subgoal using ‹list_all _ _ by simp
done

moreover have "distinct (pat_bindings p [])"
by fact

ultimately show thesis
using Cons by blast
next
show "cupcake_match_result cenv v0 pes err_v = Rval (e, p, env')"
using Cons No_match True unfolding pe = _ by auto
qed
next
case Match
with Cons show ?thesis
using True unfolding pe = _ by force
next
case Match_type_error
with Cons show ?thesis
using True unfolding pe = _ by force
qed
next
case False
hence False
using Cons unfolding pe = _ by force
thus ?thesis ..
qed
qed simp

lemma cupcake_pmatch_eq:
"is_cupcake_pat pat  pmatch_single envC s pat v0 env = cupcake_pmatch envC pat v0 env"
proof (induct rule: pmatch_single.induct)
case 4
from is_cupcake_pat.elims(2)[OF 4(2)] show ?case
proof cases
case 2
then show ?thesis
using 4(1) apply -
apply simp
apply (auto split: option.splits match_result.splits)
apply (rule Matching.fold2_cong)
apply (auto simp: fun_eq_iff split: match_result.splits)
apply (metis in_set_conv_decomp_last list.pred_inject(2) list_all_append)
done
qed simp
qed auto

lemma cupcake_match_result_eq:
"cupcake_clauses pes
match_result env s v pes err_v =
map_result (λ(e, _, env'). (e, env')) id (cupcake_match_result (c env) v pes err_v)"
by (induction pes) (auto split: match_result.splits simp: cupcake_pmatch_eq pmatch_single_equiv)

context cakeml_static_env begin

lemma cupcake_nsBind_preserve:
"is_cupcake_ns ns  is_cupcake_value v0  is_cupcake_ns (nsBind k v0 ns)"
by (cases ns) (auto elim: is_cupcake_ns.elims)

lemma cupcake_build_rec_preserve:
assumes "is_cupcake_all_env cl_env" "is_cupcake_ns env" "list_all (λ(_, _, e). is_cupcake_exp e) fs"
shows "is_cupcake_ns (build_rec_env fs cl_env env)"
proof -
have "is_cupcake_ns (foldr (λ(f, _) env'. nsBind f (Recclosure cl_env fs0 f) env') fs env)"
if "list_all (λ(_, _, e). is_cupcake_exp e) fs0"
for fs0
using ‹is_cupcake_ns env
proof (induction fs arbitrary: env)
case (Cons f fs)
show ?case
apply (cases f, simp)
apply (rule cupcake_nsBind_preserve)
apply (rule Cons.IH)
apply (rule Cons)
using that assms by auto
qed auto
thus ?thesis
unfolding build_rec_env_def
using assms
qed

lemma cupcake_v_update_preserve:
assumes "is_cupcake_all_env env" "is_cupcake_ns (f (sem_env.v env))"
shows "is_cupcake_all_env (sem_env.update_v f env)"
using assms
by (metis is_cupcake_all_env.simps(1) is_cupcake_all_envE is_cupcake_nsE sem_env.collapse sem_env.record_simps(1) sem_env.record_simps(2) sem_env.sel(2))

lemma cupcake_nsAppend_preserve: "is_cupcake_ns ns1  is_cupcake_ns ns2  is_cupcake_ns (nsAppend ns1 ns2)"
by (auto elim!: is_cupcake_ns.elims)

lemma cupcake_alist_to_ns_preserve: "list_all (is_cupcake_value  snd) env  is_cupcake_ns (alist_to_ns env)"
unfolding alist_to_ns_def
by simp

lemma cupcake_opapp_preserve:
assumes "do_opapp vs = Some (env, e)" "list_all is_cupcake_value vs"
shows "is_cupcake_all_env env" "is_cupcake_exp e"
proof -
obtain cl v0 where "vs = [cl, v0]"
using assms
by (cases vs rule: do_opapp.cases) auto
with assms have "is_cupcake_value cl" "is_cupcake_value v0"
by auto

have "is_cupcake_all_env env  is_cupcake_exp e"
using ‹do_opapp vs = _ proof (cases rule: do_opapp_cases)
case (closure env' n arg)
then show ?thesis
using ‹is_cupcake_value cl ‹is_cupcake_value v0 vs = [cl, v0]
by (auto intro: cupcake_v_update_preserve cupcake_nsBind_preserve dest:is_cupcake_all_envD(1))
next
case (recclosure env' funs name n)
hence "is_cupcake_all_env env'"
using ‹is_cupcake_value cl vs = [cl, v0] by simp
have "(name, n, e)  set funs"
using recclosure by (auto dest: map_of_SomeD)
hence "is_cupcake_exp e"
using ‹is_cupcake_value cl vs = [cl, v0] recclosure
by (auto simp: list_all_iff)
thus ?thesis
using ‹is_cupcake_all_env env' ‹is_cupcake_value cl ‹is_cupcake_value v0 vs = [cl, v0] recclosure
unfolding env = _
using cupcake_build_rec_preserve cupcake_nsBind_preserve cupcake_v_update_preserve is_cupcake_all_envD(1)
by auto
qed

thus "is_cupcake_all_env env" "is_cupcake_exp e"
by simp+
qed

context begin

lemma cup_pmatch_list_length_neq:
"length vs  length ps  Matching.fold2(λp v m. case m of
Match env  cupcake_pmatch cenv p v env
| m  m) Match_type_error ps vs m = Match_type_error"
by (induction ps vs arbitrary:m rule:List.list_induct2') auto

lemma cup_pmatch_list_nomatch:
"length vs = length ps   Matching.fold2(λp v m. case m of
Match env  cupcake_pmatch cenv p v env
| m  m) Match_type_error ps vs No_match = No_match"
by (induction ps vs  rule:List.list_induct2') auto

lemma cup_pmatch_list_typerr:
"length vs = length ps  Matching.fold2(λp v m. case m of
Match env  cupcake_pmatch cenv p v env
| m  m) Match_type_error ps vs Match_type_error = Match_type_error"
by (induction ps vs  rule:List.list_induct2') auto

private lemma cupcake_pmatch_list_preserve:
assumes " p v env. p  set ps  v  set vs  list_all (is_cupcake_value  snd) env  if_match (list_all (is_cupcake_value  snd)) (cupcake_pmatch cenv p v env)" "list_all (is_cupcake_value  snd) env"
shows "if_match (list_all (λa. is_cupcake_value (snd a))) (Matching.fold2
(λp v m. case m of
Match env  cupcake_pmatch cenv p v env
| m  m)
Match_type_error ps vs (Match env))"
using assms proof (induction ps vs arbitrary: env rule:list_induct2')
case (4 p ps v vs)
show ?case
proof (cases "cupcake_pmatch cenv p v env")
case No_match
then show ?thesis
by (cases "length ps = length vs") (auto simp:cup_pmatch_list_nomatch cup_pmatch_list_length_neq)
next
case Match_type_error
then show ?thesis
by (cases "length ps = length vs") (auto simp:cup_pmatch_list_typerr cup_pmatch_list_length_neq)
next
case (Match env')
then have env': "list_all (is_cupcake_value  snd) env'"
using 4 by fastforce
then show ?thesis
apply (cases "length ps = length vs")
using 4 Match by fastforce+
qed
qed (auto simp: comp_def)

private lemma cupcake_pmatch_preserve0:
"is_cupcake_pat pat
is_cupcake_value v0
list_all (is_cupcake_value  snd) env
cupcake_c_ns envC
if_match (list_all (is_cupcake_value  snd)) (cupcake_pmatch envC pat v0 env)"
proof (induction rule: cupcake_pmatch.induct)
case (2 cenv n ps n' t' vs env)
have p:"p  set ps  is_cupcake_pat p" for p
using 2 by (metis Ball_set is_cupcake_pat.simps(2))
have v:"v  set vs  is_cupcake_value v" for v
using 2 by (metis Ball_set is_cupcake_value.elims(2) v.distinct(11) v.distinct(13) v.inject(2))
show ?case
by (auto intro!: cupcake_pmatch_list_preserve split:if_splits option.splits) (metis 2 p v)+
qed (auto split: option.splits if_splits elim: is_cupcake_pat.elims is_cupcake_value.elims)

lemma cupcake_pmatch_preserve:
"is_cupcake_pat pat
is_cupcake_value v0
list_all (is_cupcake_value  snd) env
cupcake_c_ns envC
cupcake_pmatch envC pat v0 env = Match env'
list_all (is_cupcake_value  snd) env'"
by (metis if_match.simps(1) cupcake_pmatch_preserve0)+

end

lemma cupcake_match_result_preserve:
"cupcake_c_ns envC
cupcake_clauses pes
is_cupcake_value v
if_rval (λ(e, p, env'). is_cupcake_pat p  is_cupcake_exp e  list_all (is_cupcake_value  snd) env')
(cupcake_match_result envC v pes err_v)"
apply (induction pes)
apply (auto split: match_result.splits)
apply (rule cupcake_pmatch_preserve)
apply auto
done

lemma static_cenv_lookup:
assumes "cupcake_nsLookup static_cenv i = Some (len, b)"
obtains name where "b = TypeId (Short name)"
using assms static_cenv
apply (cases static_cenv; cases b)
apply (auto simp: list_all_iff split: prod.splits tid_or_exn.splits id0.splits dest!: map_of_SomeD elim!: ballE allE)
using static_cenv
apply (auto simp: list_all_iff split: prod.splits tid_or_exn.splits id0.splits dest!: map_of_SomeD elim!: ballE allE)
done

lemma cupcake_build_conv_preserve:
fixes v
assumes "list_all is_cupcake_value vs" "build_conv static_cenv (Some (Short i)) vs = Some v"
shows "is_cupcake_value v"
using assms
by (auto simp: build_conv.simps split: option.splits elim: static_cenv_lookup)

lemma cupcake_nsLookup_preserve:
assumes "is_cupcake_ns ns" "nsLookup ns n = Some v0"
shows "is_cupcake_value v0"
proof -
obtain vs where "list_all (is_cupcake_value  snd) vs" "ns = Bind vs []"
using assms
by (auto elim: is_cupcake_ns.elims)
show ?thesis
proof (cases n)
case (Short id)
hence "(id, v0)  set vs"
using assms unfolding ns = _ by (auto dest: map_of_SomeD)
thus ?thesis
using ‹list_all (is_cupcake_value  snd) vs
by (auto simp: list_all_iff)
next
case Long
hence "nsLookup ns n = None"
unfolding ns = _ by simp
thus ?thesis
using assms by auto
qed
qed

corollary match_all_preserve:
assumes "cupcake_match_result cenv v0 pes err_v = Rval (e, p, env')" "cupcake_c_ns cenv"
assumes "is_cupcake_value v0" "cupcake_clauses pes"
shows "list_all (is_cupcake_value  snd) env'" "is_cupcake_exp e" "is_cupcake_pat p"
proof -
from assms obtain init rest
where "pes = init @ (p, e) # rest" and "cupcake_pmatch cenv p v0 [] = Match env'"
by (elim cupcake_match_resultE)
hence "(p, e)  set pes"
by simp
thus "is_cupcake_exp e" "is_cupcake_pat p"
using assms by (auto simp: list_all_iff)

show "list_all (is_cupcake_value  snd) env'"
by (rule cupcake_pmatch_preserve[where env = "[]"]) (fact | simp)+
qed

end

fun list_all2_shortcircuit where
"list_all2_shortcircuit P (x # xs) (y # ys)  (case y of Rval _  P x y  list_all2_shortcircuit P xs ys | Rerr _  P x y)" |
"list_all2_shortcircuit P [] []  True" |
"list_all2_shortcircuit P _ _  False"

lemma list_all2_shortcircuit_induct[consumes 1, case_names nil cons_val cons_err]:
assumes "list_all2_shortcircuit P xs ys"
assumes "R [] []"
assumes "x xs y ys. P x (Rval y)  list_all2_shortcircuit P xs ys  R xs ys  R (x # xs) (Rval y # ys)"
assumes "x xs y ys. P x (Rerr y)  R (x # xs) (Rerr y # ys)"
shows "R xs ys"
using assms
proof (induction P xs ys rule: list_all2_shortcircuit.induct)
case (1 P x xs y ys)
thus ?case
by (cases y) auto
qed auto

lemma list_all2_shortcircuit_mono[mono]:
assumes "R  Q"
shows "list_all2_shortcircuit R  list_all2_shortcircuit Q"
proof
fix xs ys
assume "list_all2_shortcircuit R xs ys"
thus "list_all2_shortcircuit Q xs ys"
using assms by (induction xs ys rule: list_all2_shortcircuit_induct) auto
qed

lemma list_all2_shortcircuit_weaken: "list_all2_shortcircuit P xs ys  (xs ys. P xs ys  Q xs ys)  list_all2_shortcircuit Q xs ys"
by (metis list_all2_shortcircuit_mono predicate2I rev_predicate2D)

lemma list_all2_shortcircuit_rval[simp]:
"list_all2_shortcircuit P xs (map Rval ys)  list_all2 (λx y. P x (Rval y)) xs ys" (is "?lhs  ?rhs")
proof
assume ?lhs thus ?rhs
by (induction "map Rval ys::('b, 'c) result list" arbitrary: ys rule: list_all2_shortcircuit_induct) auto
next
assume ?rhs thus ?lhs
by (induction rule: list_all2_induct) auto
qed

inductive cupcake_evaluate_single :: "all_env  exp  (v, v) result  bool" where
con1:
"do_con_check (c env) cn (length es)
list_all2_shortcircuit (cupcake_evaluate_single env) (rev es) rs
sequence_result rs = Rval vs
build_conv (c env) cn (rev vs) = Some v0
cupcake_evaluate_single env (Con cn es) (Rval v0)" |
con2:
"¬ do_con_check (c env) cn (List.length es)
cupcake_evaluate_single env (Con cn es) (Rerr (Rabort Rtype_error))" |
con3:
"do_con_check (c env) cn (List.length es)
list_all2_shortcircuit (cupcake_evaluate_single env) (rev es) rs
sequence_result rs = Rerr err
cupcake_evaluate_single env (Con cn es) (Rerr err)" |
var1:
"nsLookup (sem_env.v env) n = Some v0  cupcake_evaluate_single env (Var n) (Rval v0)" |
var2:
"nsLookup (sem_env.v env) n = None  cupcake_evaluate_single env (Var n) (Rerr (Rabort Rtype_error))" |
fn:
"cupcake_evaluate_single env (Fun n e) (Rval (Closure env n e))" |
app1:
"list_all2_shortcircuit (cupcake_evaluate_single env) (rev es) rs
sequence_result rs = Rval vs
do_opapp (rev vs) = Some (env', e)
cupcake_evaluate_single env' e bv
cupcake_evaluate_single env (App Opapp es) bv" |
app3:
"list_all2_shortcircuit (cupcake_evaluate_single env) (rev es) rs
sequence_result rs = Rval vs
do_opapp (rev vs) = None
cupcake_evaluate_single env (App Opapp es) (Rerr (Rabort Rtype_error))" |
app6:
"list_all2_shortcircuit (cupcake_evaluate_single env) (rev es) rs
sequence_result rs = Rerr err
cupcake_evaluate_single env (App op0 es) (Rerr err)" |
mat1:
"cupcake_evaluate_single env e (Rval v0)
cupcake_match_result (c env) v0 pes Bindv = Rval (e', _, env')
cupcake_evaluate_single (env (| sem_env.v := nsAppend (alist_to_ns env') (sem_env.v env) |)) e' bv
cupcake_evaluate_single env (Mat e pes) bv" |
mat1error:
"cupcake_evaluate_single env e (Rval v0)
cupcake_match_result (c env) v0 pes Bindv = Rerr err
cupcake_evaluate_single env (Mat e pes) (Rerr err)" |
mat2:
"cupcake_evaluate_single env e (Rerr err)
cupcake_evaluate_single env (Mat e pes) (Rerr err)"

context cakeml_static_env begin

context begin

private lemma cupcake_list_preserve0:
"list_all2_shortcircuit
(λe r. cupcake_evaluate_single env e r  (is_cupcake_all_env env  is_cupcake_exp e  if_rval is_cupcake_value r)) es rs
is_cupcake_all_env env  list_all is_cupcake_exp es  sequence_result rs = Rval vs  list_all is_cupcake_value vs"
proof (induction es rs arbitrary: vs rule:list_all2_shortcircuit_induct)
case (cons_val _ _ _ rs)
thus ?case
by (cases "sequence_result rs") auto
qed auto

private lemma cupcake_single_preserve0:
"cupcake_evaluate_single env e res  is_cupcake_all_env env  is_cupcake_exp e  if_rval is_cupcake_value res"
proof (induction rule:cupcake_evaluate_single.induct)
case (con1 env cn es rs vs v0)
then obtain tid where cn: "cn = Some (Short tid)" and "list_all is_cupcake_exp (rev es)"
by (cases rule: is_cupcake_exp.cases[where x = "Con cn es"]) auto
hence "list_all is_cupcake_value (rev vs)" and "c env = static_cenv"
using cupcake_list_preserve0 con1
by (fastforce elim:is_cupcake_all_envE)+

then show ?case
using cupcake_build_conv_preserve con1 cn
by fastforce
next
case (app1 env es rs vs env' e bv)
hence "list_all is_cupcake_exp (rev es)"
by fastforce
hence "list_all is_cupcake_value (rev vs)"
using app1 cupcake_list_preserve0 by force
hence "is_cupcake_exp e" and "is_cupcake_all_env env'"
using app1 cupcake_opapp_preserve by blast+
then show ?case
using app1 by blast
next
case (mat1 env e v0 pes e' uu env' bv)
hence "cupcake_c_ns (c env)" "cupcake_clauses pes" "is_cupcake_value v0"
by (auto dest: is_cupcake_all_envD)
hence "list_all (is_cupcake_value  snd) env'" and e': "is_cupcake_exp e'"
using cupcake_match_result_preserve[where envC = "c env" and v = v0 and pes = pes and err_v = Bindv, unfolded mat1, simplified]
by auto
have "is_cupcake_all_env (update_v (λ_. nsAppend (alist_to_ns env') (sem_env.v env)) env)"
apply (rule cupcake_v_update_preserve)
apply fact
apply (rule cupcake_nsAppend_preserve)
apply (rule cupcake_alist_to_ns_preserve)