theory Build_Incredible_Tree imports Incredible_Trees Natural_Deduction begin text ‹ This theory constructs an incredible tree (with freshness checked only locally) from a natural deduction tree. › lemma image_eq_to_f: assumes "f1 ` S1 = f2 ` S2" obtains f where "⋀ x. x ∈ S2 ⟹ f x ∈ S1 ∧ f1 (f x) = f2 x" proof (atomize_elim) from assms have "∀x. x ∈ S2 ⟶ (∃ y. y ∈ S1 ∧ f1 y = f2 x)" by (metis image_iff) thus "∃f. ∀x. x ∈ S2 ⟶ f x ∈ S1 ∧ f1 (f x) = f2 x" by metis qed context includes fset.lifting begin lemma fimage_eq_to_f: assumes "f1 |`| S1 = f2 |`| S2" obtains f where "⋀ x. x |∈| S2 ⟹ f x |∈| S1 ∧ f1 (f x) = f2 x" using assms apply transfer using image_eq_to_f by metis end context Abstract_Task begin lemma build_local_iwf: fixes t :: "('form entailment × ('rule × 'form) NatRule) tree" assumes "tfinite t" assumes "wf t" shows "∃ it. local_iwf it (fst (root t))" using assms proof(induction) case (tfinite t) from ‹wf t› have "snd (root t) ∈ R" using wf.simps by blast from ‹wf t› have "eff (snd (root t)) (fst (root t)) ((fst ∘ root) |`| cont t)" using wf.simps by blast from ‹wf t› have "⋀ t'. t' |∈| cont t ⟹ wf t'" using wf.simps by blast hence IH: "⋀ Γ' t'. t' |∈| cont t ⟹ (∃it'. local_iwf it' (fst (root t')))" using tfinite(2) by blast then obtain its where its: "⋀ t'. t' |∈| cont t ⟹ local_iwf (its t') (fst (root t'))" by metis from ‹eff _ _ _› show ?case proof(cases rule: eff.cases[case_names Axiom NatRule Cut]) case (Axiom c Γ) show ?thesis proof (cases "c |∈| ass_forms") case True (* Global assumption *) then have "c ∈ set assumptions" by (auto simp add: ass_forms_def) let "?it" = "INode (Assumption c) c undefined undefined [] :: ('form, 'rule, 'subst, 'var) itree" from ‹c ∈ set assumptions› have "local_iwf ?it (Γ ⊢ c)" by (auto intro!: iwf local_fresh_check.intros) thus ?thesis unfolding Axiom.. next case False obtain s where "subst s anyP = c" by atomize_elim (rule anyP_is_any) hence [simp]: "subst s (freshen undefined anyP) = c" by (simp add: lconsts_anyP freshen_closed) let "?it" = "HNode undefined s [] :: ('form, 'rule, 'subst, 'var) itree" from ‹c |∈| Γ› False have "local_iwf ?it (Γ ⊢ c)" by (auto intro: iwfH) thus ?thesis unfolding Axiom.. qed next case (NatRule rule c ants Γ i s) from ‹natEff_Inst rule c ants› have "snd rule = c" and [simp]: "ants = f_antecedent (fst rule)" and "c ∈ set (consequent (fst rule))" by (auto simp add: natEff_Inst.simps) from ‹(fst ∘ root) |`| cont t = (λant. (λp. subst s (freshen i p)) |`| a_hyps ant |∪| Γ ⊢ subst s (freshen i (a_conc ant))) |`| ants› obtain to_t where "⋀ ant. ant |∈| ants ⟹ to_t ant |∈| cont t ∧ (fst ∘ root) (to_t ant) = ((λp. subst s (freshen i p)) |`| a_hyps ant |∪| Γ ⊢ subst s (freshen i (a_conc ant)))" by (rule fimage_eq_to_f) (rule that) hence to_t_in_cont: "⋀ ant. ant |∈| ants ⟹ to_t ant |∈| cont t" and to_t_root: "⋀ ant. ant |∈| ants ⟹ fst (root (to_t ant)) = ((λp. subst s (freshen i p)) |`| a_hyps ant |∪| Γ ⊢ subst s (freshen i (a_conc ant)))" by auto let ?ants' = "map (λ ant. its (to_t ant)) (antecedent (fst rule))" let "?it" = "INode (Rule (fst rule)) c i s ?ants' :: ('form, 'rule, 'subst, 'var) itree" from ‹snd (root t) ∈ R› have "fst rule ∈ sset rules" unfolding NatRule by (auto simp add: stream.set_map n_rules_def no_empty_conclusions ) moreover from ‹c ∈ set (consequent (fst rule))› have "c |∈| f_consequent (fst rule)" by (simp add: f_consequent_def) moreover { fix ant assume "ant ∈ set (antecedent (fst rule))" hence "ant |∈| ants" by (simp add: f_antecedent_def) from its[OF to_t_in_cont[OF this]] have "local_iwf (its (to_t ant)) (fst (root (to_t ant)))". also have "fst (root (to_t ant)) = ((λp. subst s (freshen i p)) |`| a_hyps ant |∪| Γ ⊢ subst s (freshen i (a_conc ant)))" by (rule to_t_root[OF ‹ant |∈| ants›]) also have "… = ((λh. subst s (freshen i (labelsOut (Rule (fst rule)) h))) |`| hyps_for (Rule (fst rule)) ant |∪| Γ ⊢ subst s (freshen i (a_conc ant)))" using ‹ant |∈| ants› by auto finally have "local_iwf (its (to_t ant)) ((λh. subst s (freshen i (labelsOut (Rule (fst rule)) h))) |`| hyps_for (Rule (fst rule)) ant |∪| Γ ⊢ subst s (freshen i (a_conc ant)))". } moreover from NatRule(5,6) have "local_fresh_check (Rule (fst rule)) i s (Γ ⊢ subst s (freshen i c))" by (fastforce intro!: local_fresh_check.intros simp add: all_local_vars_def) ultimately have "local_iwf ?it ((Γ ⊢ subst s (freshen i c)))" by (intro iwf ) (auto simp add: list_all2_map2 list_all2_same) thus ?thesis unfolding NatRule.. next case (Cut Γ con) obtain s where "subst s anyP = con" by atomize_elim (rule anyP_is_any) hence [simp]: "subst s (freshen undefined anyP) = con" by (simp add: lconsts_anyP freshen_closed) from ‹(fst ∘ root) |`| cont t = {|Γ ⊢ con|}› obtain t' where "t' |∈| cont t" and [simp]: "fst (root t') = (Γ ⊢ con)" by (cases "cont t") auto from ‹t' |∈| cont t› obtain "it'" where "local_iwf it' (Γ ⊢ con)" using IH by force let "?it" = "INode Helper anyP undefined s [it'] :: ('form, 'rule, 'subst, 'var) itree" from ‹local_iwf it' (Γ ⊢ con)› have "local_iwf ?it (Γ ⊢ con)" by (auto intro!: iwf local_fresh_check.intros) thus ?thesis unfolding Cut.. qed qed definition to_it :: "('form entailment × ('rule × 'form) NatRule) tree ⇒ ('form,'rule,'subst,'var) itree" where "to_it t = (SOME it. local_iwf it (fst (root t)))" lemma iwf_to_it: assumes "tfinite t" and "wf t" shows "local_iwf (to_it t) (fst (root t))" unfolding to_it_def using build_local_iwf[OF assms] by (rule someI2_ex) end end