# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1264372887 -3600
# Node ID 7be9b054f6721ad1013d7b6141ef5e0eb8f159c2
# Parent  2cb5745f403eb35b0953c76f2962a8c56876bb5e
test with splits

diff -r 2cb5745f403e -r 7be9b054f672 Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Sat Jan 23 17:25:18 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Sun Jan 24 23:41:27 2010 +0100
@@ -2,6 +2,52 @@
 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List
 begin
 
+ML_command "ProofContext.debug := false"
+ML_command "ProofContext.verbose := false"
+
+ML {*
+val ctxt0 = @{context}
+val ty = Syntax.read_typ ctxt0 "bool"  
+val ctxt1 = Variable.declare_typ ty ctxt0 
+val trm = Syntax.parse_term ctxt1 "A \<and> B"
+val trm' = Syntax.type_constraint ty trm
+val trm'' = Syntax.check_term ctxt1 trm'
+val ctxt2 = Variable.declare_term trm'' ctxt1 
+*}
+
+term "split"
+
+term "Ex1 (\<lambda>(x, y). P x y)" 
+
+lemma "(Ex1 (\<lambda>(x, y). P x y)) \<Longrightarrow> (\<exists>! x. \<exists>! y. P x y)"
+apply(erule ex1E)
+apply(case_tac x)
+apply(clarify)
+apply(rule_tac a="aa" in ex1I)
+apply(rule ex1I)
+apply(assumption)
+apply(blast)
+apply(blast)
+done
+
+(*
+lemma "(\<exists>! x. \<exists>! y. P x y) \<Longrightarrow> (Ex1 (\<lambda>(x, y). P x y))"
+apply(erule ex1E)
+apply(erule ex1E)
+apply(rule_tac a="(x, y)" in ex1I)
+apply(clarify)
+apply(case_tac xa)
+apply(clarify)
+
+apply(rule ex1I)
+apply(assumption)
+apply(blast)
+apply(blast)
+done
+
+apply(metis)
+*)
+
 ML {* open Quotient_Term *}
 
 ML {*
diff -r 2cb5745f403e -r 7be9b054f672 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Sat Jan 23 17:25:18 2010 +0100
+++ b/Quot/Examples/FSet.thy	Sun Jan 24 23:41:27 2010 +0100
@@ -1,5 +1,5 @@
 theory FSet
-imports "../QuotMain" "../QuotList" List
+imports "../QuotMain" "../QuotList" "../QuotProd" List
 begin
 
 inductive
@@ -377,6 +377,46 @@
 apply(assumption)
 done
 
+lemma [quot_respect]:
+  "((op \<approx> ===> op \<approx> ===> op =) ===> prod_rel op \<approx> op \<approx> ===> op =) split split"
+apply(simp)
+done
+
+thm quot_preserve
+term split
+
+
+lemma [quot_preserve]:
+  shows "(((abs_fset ---> abs_fset ---> id) ---> prod_fun rep_fset rep_fset ---> id) split) = split"
+apply(simp add: expand_fun_eq)
+apply(simp add: Quotient_abs_rep[OF Quotient_fset])
+done
+
+
+lemma test: "All (\<lambda>(x::'a list, y). x = y)"
+sorry
+
+lemma  "All (\<lambda>(x::'a fset, y). x = y)"
+apply(lifting test)
+apply(cleaning)
+thm all_prs
+apply(rule all_prs)
+apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1*})
+done
+
+lemma test2: "Ex (\<lambda>(x::'a list, y). x = y)"
+sorry
+
+lemma  "Ex (\<lambda>(x::'a fset, y). x = y)"
+apply(lifting test2)
+apply(cleaning)
+apply(rule ex_prs)
+apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1*})
+done
+
+ML {* @{term "Ex (\<lambda>(x::'a fset, y). x = y)"} *}
+
+
 
 
 end
diff -r 2cb5745f403e -r 7be9b054f672 Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Sat Jan 23 17:25:18 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Sun Jan 24 23:41:27 2010 +0100
@@ -71,6 +71,9 @@
 | a3: "\<exists>pi::name prm. (rfv t - {a} = rfv s - {b} \<and> (rfv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b)
        \<Longrightarrow> rLam a t \<approx> rLam b s"
 
+
+
+
 (* should be automatic with new version of eqvt-machinery *)
 lemma alpha_eqvt:
   fixes pi::"name prm"
@@ -573,6 +576,17 @@
 lemma term1_hom_rsp:
   "\<lbrakk>(alpha ===> alpha ===> op =) f_app f_app; ((op = ===> alpha) ===> op =) f_lam f_lam\<rbrakk>
        \<Longrightarrow> (alpha ===> op =) (term1_hom f_var f_app f_lam) (term1_hom f_var f_app f_lam)"
+apply(simp)
+apply(rule allI)+
+apply(rule impI)
+apply(erule alpha.induct)
+apply(auto)[1]
+apply(auto)[1]
+apply(simp)
+apply(erule conjE)+
+apply(erule exE)+
+apply(erule conjE)+
+apply(clarify)
 sorry
 
 lemma hom: "
diff -r 2cb5745f403e -r 7be9b054f672 Quot/Examples/SigmaEx.thy
--- a/Quot/Examples/SigmaEx.thy	Sat Jan 23 17:25:18 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Sun Jan 24 23:41:27 2010 +0100
@@ -113,7 +113,8 @@
 translations
   "\<exists>\<exists> x. P"   == "Ex (%x. P)"
 
-lemma split_rsp[quot_respect]: "((R1 ===> R2 ===> op =) ===> (prod_rel R1 R2) ===> op =) split split"
+lemma split_rsp[quot_respect]: 
+  "((R1 ===> R2 ===> op =) ===> (prod_rel R1 R2) ===> op =) split split"
 by auto
 
 lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar"
@@ -130,6 +131,8 @@
 lemma operm_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_obj) op \<bullet> op \<bullet>"
 sorry
 
+  
+
 lemma liftd: "
 \<exists>\<exists>(hom_o, (hom_d, (hom_e, hom_m))).
 (
diff -r 2cb5745f403e -r 7be9b054f672 Quot/ROOT.ML
--- a/Quot/ROOT.ML	Sat Jan 23 17:25:18 2010 +0100
+++ b/Quot/ROOT.ML	Sun Jan 24 23:41:27 2010 +0100
@@ -11,4 +11,5 @@
     "Examples/LFex",
     "Examples/LamEx",
     "Examples/LarryDatatype",
-    "Examples/LarryInt"];
+    "Examples/LarryInt",
+    "Examples/Terms"];
diff -r 2cb5745f403e -r 7be9b054f672 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Sat Jan 23 17:25:18 2010 +0100
+++ b/Quot/quotient_typ.ML	Sun Jan 24 23:41:27 2010 +0100
@@ -264,6 +264,8 @@
 let
   fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) =
   let
+    (*val rty = Syntax.read_typ lthy rty_str*)
+    
     val rty = Syntax.read_typ lthy rty_str
     val rel = Syntax.read_term lthy rel_str 
   in