theory Term4

imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List"

begin

atom_decl name

section {*** lam with indirect list recursion ***}

datatype rtrm4 =

  rVr4 "name"

| rAp4 "rtrm4" "rtrm4 list"

| rLm4 "name" "rtrm4"  --"bind (name) in (trm)"

print_theorems

thm rtrm4.recs

(* there cannot be a clause for lists, as *)

(* permutations are  already defined in Nominal (also functions, options, and so on) *)

setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *}

print_theorems

(* "repairing" of the permute function *)

lemma repaired:

  fixes ts::"rtrm4 list"

  shows "permute_rtrm4_list p ts = p \<bullet> ts"

  apply(induct ts)

  apply(simp_all)

  done

thm permute_rtrm4_permute_rtrm4_list.simps

lemmas rawperm=permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]

local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4")

  [[[], [], [(NONE, 0, 1, AlphaGen)]], [[], []] ] [] *}

print_theorems

lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4"

apply (rule ext)+

apply (induct_tac x xa rule: list_induct2')

apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros)

apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)

apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)

apply rule

apply (erule alpha_rtrm4_list.cases)

apply simp_all

apply (rule alpha_rtrm4_alpha_rtrm4_list.intros)

apply simp_all

done

(* We need sth like:

lemma fix3: "fv_rtrm4_list = set o map fv_rtrm4" *)

notation

  alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and

  alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)

thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *}

thm alpha4_inj

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}

thm alpha4_inj_no

local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4_fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *}

thm eqvts(1-2)

local_setup {*

(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []),

  build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} ctxt 1) ctxt) ctxt))

*}

lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2]

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []),

  build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj_no} ctxt) ctxt)) *}

thm alpha4_reflp

ML build_equivps

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []),

  (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *}

lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2]

quotient_type 

  trm4 = rtrm4 / alpha_rtrm4

(*and

  trm4list = "rtrm4 list" / alpha_rtrm4_list*)

  by (simp_all add: alpha4_equivp)

local_setup {*

(fn ctxt => ctxt

 |> snd o (Quotient_Def.quotient_lift_const [] ("Vr4", @{term rVr4}))

 |> snd o (Quotient_Def.quotient_lift_const [@{typ "trm4"}] ("Ap4", @{term rAp4}))

 |> snd o (Quotient_Def.quotient_lift_const [] ("Lm4", @{term rLm4}))

 |> snd o (Quotient_Def.quotient_lift_const [] ("fv_trm4", @{term fv_rtrm4})))

*}

print_theorems

lemma fv_rtrm4_rsp:

  "xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya"

  "x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y"

  apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts)

  apply (simp_all add: alpha_gen)

done

local_setup {* snd o prove_const_rsp [] @{binding fv_rtrm4_rsp'} [@{term fv_rtrm4}]

  (fn _ => asm_full_simp_tac (@{simpset} addsimps @{thms fv_rtrm4_rsp}) 1) *}

print_theorems

local_setup {* snd o prove_const_rsp [] @{binding rVr4_rsp} [@{term rVr4}]

  (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *}

local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}]

  (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *}

lemma [quot_respect]:

  "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"

  by (simp add: alpha4_inj)

(* Maybe also need: @{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"} *)

local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp}

  [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}]

  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *}

print_theorems

setup {* define_lifted_perms [@{typ trm4}] ["Term4.trm4"] [("permute_trm4", @{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"})] @{thms permute_rtrm4_permute_rtrm4_list_zero permute_rtrm4_permute_rtrm4_list_append} *}

print_theorems

lemma bla: "(Ap4 trm4 list = Ap4 trm4a lista) =

  (trm4 = trm4a \<and> list_rel (op =) list lista)"

  by (lifting alpha4_inj(2))

thm bla[simplified list_rel_eq]

ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(1)} *}

ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(2)} *}

ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(3)[unfolded alpha_gen]} *}

ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *}

.

(*lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]*)

end